1. 20 Dec, 2017 1 commit
    • Sylvain Dailler's avatar
      Cherry picked from a commit of Julien Thierry that aims at improving the · 4756c1cd
      Sylvain Dailler authored
      Coq printer.
      Also adding the "pretty-printed" generated realization.
      
      
      
      N604-045 Coq code easier to read
      
      * src/printer/coq.ml
      Added indentation in Why3's Coq printer using the OCaml Format pretty
      printing module.
      Changed the display of logic formulas and terms only.
      
      (cherry picked from commit 3453a65e0e5fca7e3aa16e22915ee3f079daf1c6)
      
      Conflicts:
      	src/printer/coq.ml
      	src/transform/gnat_split_conj.ml
      4756c1cd
  2. 19 Dec, 2017 3 commits
    • Sylvain Dailler's avatar
      Fixes #58 · 373a7bc9
      Sylvain Dailler authored
      Remove now selects the parent of the removed node when a selected node is
      contained in the removed subtree.
      
      Adding a function that check a request is not referring to obsolete
      node_id in itp_server.ml. If such a request is found, the error that owuld
      have been generated is not sent to the ide.
      373a7bc9
    • Sylvain Dailler's avatar
      79da7958
    • Sylvain Dailler's avatar
      Fixes #59 · 3fce61d8
      Sylvain Dailler authored
      Adding random (to be set) shortcut to the functions: next unproven goal,
      expand, expand_all, collapse, parent, first_child. These can be accessed
      from the command line by typing the command (list_ide_command is for help
      on these commands).
      Fixing shortcuts with ~key instead of add_accelerator.
      [get_first_unproven_goal_around cn] now returns a different node from cn
      and, if a brother of cn is returned, it returns preferably one placed
      after cn in the tree.
      3fce61d8
  3. 15 Dec, 2017 2 commits
  4. 12 Dec, 2017 5 commits
  5. 11 Dec, 2017 14 commits
  6. 08 Dec, 2017 15 commits