aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.mli
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Emilio Jesus Gallego Arias2018-02-05
* [stm] Move options to a per-document record.Gravatar Emilio Jesus Gallego Arias2018-01-31
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
* [flags] [stm] Reorganize flags.Gravatar Emilio Jesus Gallego Arias2017-12-11
* [plugins] Prepare plugin API for functional handling of state.Gravatar Emilio Jesus Gallego Arias2017-11-19
* [stm] Move interpretation state to VernacentriesGravatar Emilio Jesus Gallego Arias2017-10-17
* [stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Gravatar Emilio Jesus Gallego Arias2017-10-11
* [stm] Switch to a functional APIGravatar Emilio Jesus Gallego Arias2017-10-06
* [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
* Add XML protocol support for Wait.Gravatar Maxime Dénès2017-09-19
* [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* [stm] Port the toplevel to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [stm] Move main parsing entry point to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [stm] remove process_error_hookGravatar Emilio Jesus Gallego Arias2017-04-07
* [stm] remove tactic_being_run hookGravatar Emilio Jesus Gallego Arias2017-04-07
* [stm] Remove unused legacy stm interface.Gravatar Emilio Jesus Gallego Arias2017-02-15
* [stm] Reenable Show Script command.Gravatar Emilio Jesus Gallego Arias2017-02-15
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
* [stm] Fix record field name clash.Gravatar Emilio Jesus Gallego Arias2016-10-18
* STM: proof block detection made optional + simple testGravatar Enrico Tassi2016-06-06
* STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
* STM: invalid states are first class citizensGravatar Enrico Tassi2016-06-06
* Move serialization functions out of StmGravatar Emilio Jesus Gallego Arias2016-06-02
* typosGravatar Enrico Tassi2016-05-23
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* | CLEANUP: removing unnecessary wrapperGravatar Matej Kosik2016-01-11
|/
* Add a way to get the right fix_exn in external vernacular commandsGravatar Matthieu Sozeau2015-10-30
* STM: Added functions for saving and restoring the internal stateGravatar Alec Faithfull2015-10-09
* STM: Pass exception information to unreachable_state_hook functionsGravatar Alec Faithfull2015-10-09
* STM: for PIDE based UIs, edit_at requires no Reach.known_stateGravatar Enrico Tassi2015-10-08
* Hook when state arrives on master.Gravatar Enrico Tassi2015-01-07
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* STM: simplify state managementGravatar Enrico Tassi2014-12-17
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* STM: hook called whenever a state is unreachableGravatar Enrico Tassi2014-11-27
* AsyncTaskQueue: parsin can also happen in the workers nowGravatar Enrico Tassi2014-11-27
* STM: new API async_queryGravatar Enrico Tassi2014-11-27
* STM: put hooks in key events to let plugins customize the feedbackGravatar Enrico Tassi2014-11-27
* STM: code refactoringGravatar Enrico Tassi2014-11-03
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
* STM: new worker for queriesGravatar Enrico Tassi2014-10-31
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* XML pretty printing for AST (work by François Poulain, project DoCoq)Gravatar Enrico Tassi2014-09-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 23:36:02 +0000