diff options
| -rw-r--r-- | isar/ProofGeneral.ML | 41 |
1 files changed, 0 insertions, 41 deletions
diff --git a/isar/ProofGeneral.ML b/isar/ProofGeneral.ML deleted file mode 100644 index 8cf11f2f..00000000 --- a/isar/ProofGeneral.ML +++ /dev/null @@ -1,41 +0,0 @@ -(* - Isabelle/Isar configuration for Proof General. - - Author: David Aspinall <da@dcs.ed.ac.uk> - Contact: Isabelle maintainer <isabelle@dcs.ed.ac.uk> - - ProofGeneral.ML,v 2.16 1998/11/03 16:29:30 da Exp - -MMW: I have temporarily removed the theory loader patches, since it -kept crashing on me. -*) - - -(** configure output channels to decorate output **) - -(*messages*) -writeln_fn := - (std_output o suffix "\n" o enclose (oct_char "360") (oct_char "361")); -warning_fn := - (std_output o suffix "\n" o enclose (oct_char "362") (oct_char "363") o prefix_lines "### "); -error_fn := - (std_output o suffix "\n" o enclose (oct_char "364") (oct_char "365") o prefix_lines "*** "); - -(*prompts*) -Source.decorate_prompt_fn := (fn s => s ^ oct_char "372"); - -(*theory / proof state*) -current_goals_markers := - let - val begin_state = oct_char "366"; - val end_state= oct_char "367"; - val begin_goal = oct_char "370"; - in (begin_state, end_state, begin_goal) end; - -Toplevel.print_state_fn := - (Library.setmp writeln_fn (std_output o suffix "\n") Toplevel.print_state_default); - - -print_mode := ["ProofGeneral"]; - -Isar.main(); |