equal
deleted
inserted
replaced
1216 (* provercontrol *) |
1216 (* provercontrol *) |
1217 | "proverinit" => isar_restart () |
1217 | "proverinit" => isar_restart () |
1218 | "proverexit" => isarcmd "quit" |
1218 | "proverexit" => isarcmd "quit" |
1219 | "startquiet" => isarcmd "disable_pr" |
1219 | "startquiet" => isarcmd "disable_pr" |
1220 | "stopquiet" => isarcmd "enable_pr" |
1220 | "stopquiet" => isarcmd "enable_pr" |
1221 | "pgmlsymbolson" => change print_mode (insert (op =) Symbol.xsymbolsN) |
1221 | "pgmlsymbolson" => change print_mode (fn mode => |
|
1222 remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN]) |
1222 | "pgmlsymbolsoff" => change print_mode (remove (op =) Symbol.xsymbolsN) |
1223 | "pgmlsymbolsoff" => change print_mode (remove (op =) Symbol.xsymbolsN) |
1223 (* properproofcmd: proper commands which belong in script *) |
1224 (* properproofcmd: proper commands which belong in script *) |
1224 (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *) |
1225 (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *) |
1225 (* NB: Isar doesn't make lemma name of goal accessible during proof *) |
1226 (* NB: Isar doesn't make lemma name of goal accessible during proof *) |
1226 | "opengoal" => isarscript data |
1227 | "opengoal" => isarscript data |