From 8a38cb65a774da958cd02d77803c0f69d40ab11e Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Fri, 21 May 1999 17:10:22 +0000 Subject: made part of the Isabelle sources; --- isar/ProofGeneral.ML | 41 ----------------------------------------- 1 file changed, 41 deletions(-) delete mode 100644 isar/ProofGeneral.ML 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 - Contact: Isabelle maintainer - - 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(); -- cgit v1.2.3