git.iko.soy/Idris-dev
on d9c3c21 help sign in
history ofsrc/Idris/REPLParser.hs
all commits
583cc43Add ability to set ANSI italicsDavid Christiansen 73bdc53Refactoring of parser to Trifecta, documenting and updating some items/fixing some issues.Ahmad Salim Al-Sibahi 8125e03Add support for init scriptsDavid Christiansen d759b26Parser fix for colour setting commandsDavid Christiansen fe20bf1Allow colour options from REPLDavid Christiansen efa3f8fIgnore initial whitespace and comments in REPLMelvar Chen 3aa61b3Delete unused codeBenjamin Saunders 8af32d4squash potential space leaks by using strict foldlraichoo 75e0141add command to change current directoryHannes Mehnert 3262127Dynamically load C libraries in REPLDavid Christiansen c020e50javascript: split javascript and node targetraichoo 12dcee5Merge commit '06fffa315afc0d883f36a6ce971df1123aa6d8e3' into javascriptIrene Knapp 06fffa3JavaScript stuff.Irene Knapp fab5d73Adding support for Windows MingW32chetant 1ccd94aSyntax for documentation comments and :doc REPL commandEdwin Brady 671d39aFix name clashes between holes and bound variablesEdwin Brady 665676bAdded :l and :m commands to REPLEdwin Brady f2af303:addproof now adds most recent proof if no argument given Consistent with old behaviour, and with tutorialEdwin Brady 5a6299bUnification fix Specifically to stop it filling in things which are given by the programmer (caused by a bug replacing nullary constructors with terms!)Edwin Brady 8063cfdAdded --dumpcases <file> option for dumping case trees on compilingEdwin Brady 0679225Tweak match compilation (right to left, rather than l to r) Now matches on values before indices, to give a chance of erasing indices.Edwin Brady 16a6c95Set up for adding new compiler back ends more easilyEdwin Brady 7f2d76cenhanced proof handelingraichoo b8815e2added proof listraichoo 0887715Output C file (not finished...)Edwin Brady e1c7b0fAdd "--errorcontext" flag, and :set and :unset in the REPL. :set errorcontext will cause unification errors to also dump the current context.Edwin Brady b01a78eQuick hack at :info for exploring type classesEdwin Brady 9864c25Add :total commandEdwin Brady baaba44Run-time forcing optimisationEdwin Brady b20f2f8Tinker with compiler interfaceEdwin Brady acb1f19Add :a comment, to add most recent proof script to source fileEdwin Brady b26716aCollect cumulativity constraints on universesEdwin Brady ffc64e3Add mechanism for simplification and function optionsEdwin Brady d676ca6Added -o option, and :exec and :t at the REPLEdwin Brady 22546bc:r and :e at the REPL.Edwin Brady 551548cBeginning theorem prover interfaceEdwin Brady 7c4f79cSome progress towards specialisationEdwin Brady b8a2bbfAdd :log to REPLEdwin Brady 12bd089Added lifting of unsolved metavariables to global functionsEdwin Brady 20861ecEnough Epic to compile 'hello world' (but not much else yet...)Edwin Brady 9fe3473Added using blocksEdwin Brady f85d1f0:ttshellEdwin Brady 82585e7Some ghc 6.12 compatibilityEdwin Brady 3b297bcParsing declarations, keeping track of fixitiesEdwin Brady 50d24ecStart of a REPL and main program with argument processingEdwin Brady