• Sylvain's avatar
    Merge branch 'external_printer' · 974ef24c
    Sylvain authored
    This is a proof of concept of the external printing/parsing. This works by
    adding externally defined (from Pretty) elements to the standard
    printing/parsing. We use the example of the Python plugin to show how it
    works:
    
    - the tasks should contain new notations (example python: /\ replaced by "and")
    - the new notations can be used in the transformations (example python:
      "assert (0 == 0 and b > 1)"
    
    The file format contained in the session is used to decide which external
    parser/printer to use. These are registered in a similar way that language,
    parser, or transformations are registered. For example, a goal whose ancestor
    is a python file (according to the file format inside the session) will be
    printed with the Python external printer; and transformations originating
    from this goal will be parsed with the same language.
    974ef24c
Name
Last commit
Last update
..
mach Loading commit data...
algebra.mlw Loading commit data...
appmap.mlw Loading commit data...
array.mlw Loading commit data...
bag.mlw Loading commit data...
bintree.mlw Loading commit data...
bool.mlw Loading commit data...
bv.mlw Loading commit data...
cursor.mlw Loading commit data...
debug.mlw Loading commit data...
exn.mlw Loading commit data...
floating_point.mlw Loading commit data...
for_drivers.mlw Loading commit data...
function.mlw Loading commit data...
graph.mlw Loading commit data...
hashtbl.mlw Loading commit data...
ieee_float.mlw Loading commit data...
impmap.mlw Loading commit data...
int.mlw Loading commit data...
io.mlw Loading commit data...
list.mlw Loading commit data...
map.mlw Loading commit data...
matrix.mlw Loading commit data...
microc.mlw Loading commit data...
null.mlw Loading commit data...
number.mlw Loading commit data...
ocaml.mlw Loading commit data...
option.mlw Loading commit data...
pigeon.mlw Loading commit data...
pqueue.mlw Loading commit data...
python.mlw Loading commit data...
queue.mlw Loading commit data...
random.mlw Loading commit data...
real.mlw Loading commit data...
ref.mlw Loading commit data...
regexp.mlw Loading commit data...
relations.mlw Loading commit data...
seq.mlw Loading commit data...
set.mlw Loading commit data...
stack.mlw Loading commit data...
string.mlw Loading commit data...
sum.mlw Loading commit data...
tptp.mlw Loading commit data...
tree.mlw Loading commit data...
witness.mlw Loading commit data...