--- a/src/Pure/Interface/ROOT.ML Wed Jan 16 17:53:22 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(* Title: Pure/Interface/ROOT.ML
- ID: $Id$
-
-Specific support for user-interfaces.
-*)
-
-use "proof_general.ML";
--- a/src/Pure/Interface/proof_general.ML Wed Jan 16 17:53:22 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,364 +0,0 @@
-(* Title: Pure/Interface/proof_general.ML
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
- License: GPL (GNU GENERAL PUBLIC LICENSE)
-
-Isabelle configuration for Proof General (see http://www.proofgeneral.org).
-*)
-
-signature PROOF_GENERAL =
-sig
- val setup: (theory -> theory) list
- val update_thy_only: string -> unit
- val try_update_thy_only: string -> unit
- val inform_file_processed: string -> unit
- val inform_file_retracted: string -> unit
- val thms_containing: string list -> unit
- val help: unit -> unit
- val show_context: unit -> theory
- val kill_goal: unit -> unit
- val repeat_undo: int -> unit
- val isa_restart: unit -> unit
- val init: bool -> unit
- val write_keywords: string -> unit
-end;
-
-structure ProofGeneral: PROOF_GENERAL =
-struct
-
-(* print modes *)
-
-val proof_generalN = "ProofGeneral";
-val xsymbolsN = "xsymbols";
-
-val pgmlN = "PGML";
-fun pgml () = pgmlN mem_string ! print_mode;
-
-
-(* text output *)
-
-local
-
-fun xsymbols_output s =
- if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
- let val syms = Symbol.explode s
- in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end
- else (s, real (size s));
-
-fun pgml_output (s, len) =
- if pgml () then (XML.text s, len)
- else (s, len);
-
-in
-
-fun setup_xsymbols_output () =
- Symbol.add_mode proof_generalN (pgml_output o xsymbols_output, Symbol.default_indent);
-
-end;
-
-
-(* token translations *)
-
-local
-
-val end_tag = oct_char "350";
-val class_tag = ("class", oct_char "351");
-val tfree_tag = ("tfree", oct_char "352");
-val tvar_tag = ("tvar", oct_char "353");
-val free_tag = ("free", oct_char "354");
-val bound_tag = ("bound", oct_char "355");
-val var_tag = ("var", oct_char "356");
-val skolem_tag = ("skolem", oct_char "357");
-
-fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
-
-fun tagit (kind, bg_tag) x =
- (if pgml () then xml_atom kind x else bg_tag ^ x ^ end_tag,
- real (Symbol.length (Symbol.explode x)));
-
-fun free_or_skolem x =
- (case try Syntax.dest_skolem x of
- None => tagit free_tag x
- | Some x' => tagit skolem_tag x');
-
-fun var_or_skolem s =
- (case Syntax.read_var s of
- Var ((x, i), _) =>
- (case try Syntax.dest_skolem x of
- None => tagit var_tag s
- | Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
- | _ => tagit var_tag s);
-
-val proof_general_trans =
- Syntax.tokentrans_mode proof_generalN
- [("class", tagit class_tag),
- ("tfree", tagit tfree_tag),
- ("tvar", tagit tvar_tag),
- ("free", free_or_skolem),
- ("bound", tagit bound_tag),
- ("var", var_or_skolem)];
-
-in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
-
-
-
-(* messages and notification *)
-
-local
-
-fun decorated_output bg en prfx =
- writeln_default o enclose bg en o prefix_lines prfx;
-
-fun message kind bg en prfx s =
- if pgml () then writeln_default (XML.element kind [] [prefix_lines prfx s])
- else decorated_output bg en prfx s;
-
-val notify = message "notify" (oct_char "360") (oct_char "361") "";
-
-in
-
-fun setup_messages () =
- (writeln_fn := message "output" "" "" "";
- priority_fn := message "information" (oct_char "360") (oct_char "361") "";
- tracing_fn := message "tracing" (oct_char "360" ^ oct_char "375") (oct_char "361") "";
- warning_fn := message "warning" (oct_char "362") (oct_char "363") "### ";
- error_fn := message "error" (oct_char "364") (oct_char "365") "*** ");
-
-fun tell_clear_goals () = notify "Proof General, please clear the goals buffer.";
-fun tell_clear_response () = notify "Proof General, please clear the response buffer.";
-fun tell_file msg path = notify ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
-
-end;
-
-
-(* theory / proof state output *)
-
-local
-
-fun tmp_markers f =
- setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f ();
-
-fun statedisplay prts =
- writeln_default (XML.element "statedisplay" [] [Pretty.string_of (Pretty.chunks prts)]);
-
-fun print_current_goals n m st =
- if pgml () then statedisplay (Display.pretty_current_goals n m st)
- else tmp_markers (fn () => Display.print_current_goals_default n m st);
-
-fun print_state b st =
- if pgml () then statedisplay (Toplevel.pretty_state b st)
- else tmp_markers (fn () => Toplevel.print_state_default b st);
-
-in
-
-fun setup_state () =
- (Display.print_current_goals_fn := print_current_goals;
- Toplevel.print_state_fn := print_state;
- Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
-
-end;
-
-
-(* theory loader actions *)
-
-local
-
-fun add_master_files name files =
- let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
- in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
-
-fun trace_action action name =
- if action = ThyInfo.Update then
- seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name)
- else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
- seq (tell_file "you can unlock the file") (add_master_files name (ThyInfo.loaded_files name))
- else ();
-
-in
- fun setup_thy_loader () = ThyInfo.add_hook trace_action;
- fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
-end;
-
-
-(* prepare theory context *)
-
-val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
-val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
-
-fun which_context () =
- (case Context.get_context () of
- Some thy => " Using current (dynamic!) one: " ^
- (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
- | None => "");
-
-fun try_update_thy_only file =
- ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
- let val name = thy_name file in
- if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name
- else warning ("Unkown theory context of ML file." ^ which_context ())
- end) ();
-
-
-(* get informed about files *)
-
-val touch_child_thys = ThyInfo.if_known_thy ThyInfo.touch_child_thys;
-
-val inform_file_processed = touch_child_thys o thy_name;
-val inform_file_retracted = touch_child_thys o thy_name;
-
-fun proper_inform_file_processed file state =
- let val name = thy_name file in
- touch_child_thys name;
- if not (Toplevel.is_toplevel state) then
- warning ("Not at toplevel -- cannot register theory " ^ quote name)
- else Library.transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
- (warning msg; warning ("Failed to register theory " ^ quote name))
- end;
-
-
-(* misc commands for ProofGeneral/isa *)
-
-fun thms_containing ss =
- let
- val thy = the_context ();
- fun read_term s = Thm.term_of (Thm.read_cterm (Theory.sign_of thy) (s, TypeInfer.logicT));
- in ThmDatabase.print_thms_containing thy (map read_term ss) end;
-
-val welcome = priority o Session.welcome;
-val help = welcome;
-val show_context = Context.the_context;
-
-fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
-
-fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
-
-fun repeat_undo 0 = ()
- | repeat_undo 1 = undo ()
- | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
-
-
-(* restart top-level loop (keeps most state information) *)
-
-local
-
-fun restart isar =
- (if isar then tell_clear_goals () else kill_goal ();
- tell_clear_response ();
- welcome ());
-
-in
-
-fun isa_restart () = restart false;
-fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
-
-end;
-
-
-(* outer syntax *)
-
-local structure P = OuterParse and K = OuterSyntax.Keyword in
-
-val old_undoP = (*same name for compatibility with PG/Isabelle99*)
- OuterSyntax.improper_command "undo" "undo last command (no output)" K.control
- (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
-
-val undoP =
- OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
- (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
-
-val context_thy_onlyP =
- OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
- (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
-
-val try_context_thy_onlyP =
- OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
- (P.name >> (Toplevel.no_timing oo
- (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
-
-val restartP =
- OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
- (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
-
-val kill_proofP =
- OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
- (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
-
-val inform_file_processedP =
- OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
- (P.name >> (Toplevel.no_timing oo
- (fn name => Toplevel.keep (proper_inform_file_processed name))));
-
-val inform_file_retractedP =
- OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
- (P.name >> (Toplevel.no_timing oo
- (fn name => Toplevel.imperative (fn () => inform_file_retracted name))));
-
-fun init_outer_syntax () = OuterSyntax.add_parsers
- [old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
- inform_file_processedP, inform_file_retractedP];
-
-end;
-
-
-(* init *)
-
-val initialized = ref false;
-
-fun init isar =
- (conditional (not (! initialized)) (fn () =>
- (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
- setup_xsymbols_output ();
- setup_messages ();
- setup_state ();
- setup_thy_loader ();
- set initialized; ()));
- sync_thy_loader ();
- print_mode := proof_generalN :: (! print_mode \ proof_generalN);
- set quick_and_dirty;
- ThmDeps.enable ();
- if isar then ml_prompts "ML> " "ML# "
- else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
- if isar then (welcome (); Isar.sync_main ()) else isa_restart ());
-
-
-
-(** generate keyword classification file **)
-
-local
-
-val regexp_meta = explode ".*+?[]^$";
-val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
-
-fun defconst name strs =
- "\n(defconst isar-keywords-" ^ name ^
- "\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n";
-
-fun make_elisp_commands commands kind =
- defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
-
-fun make_elisp_syntax (keywords, commands) =
- ";;\n\
- \;; Keyword classification tables for Isabelle/Isar.\n\
- \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
- \;;\n\
- \;; $" ^ "Id$\n\
- \;;\n" ^
- defconst "major" (map #1 commands) ^
- defconst "minor" (filter Syntax.is_identifier keywords) ^
- implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
- "\n(provide 'isar-keywords)\n";
-
-in
-
-fun write_keywords s =
- (init_outer_syntax ();
- File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
- (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
-
-end;
-
-
-end;
-
-(*a hack for Proof General 3.2 to avoid problems with escapes in ML commands*)
-infix \\\\ val op \\\\ = op \\;
--- a/src/Pure/IsaMakefile Wed Jan 16 17:53:22 2002 +0100
+++ b/src/Pure/IsaMakefile Wed Jan 16 20:57:02 2002 +0100
@@ -28,7 +28,7 @@
General/name_space.ML General/object.ML General/path.ML \
General/position.ML General/pretty.ML General/scan.ML General/seq.ML \
General/source.ML General/symbol.ML General/table.ML General/url.ML \
- General/xml.ML Interface/ROOT.ML Interface/proof_general.ML \
+ General/xml.ML \
Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML \
Isar/auto_bind.ML Isar/calculation.ML Isar/comment.ML \
Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML \
@@ -51,7 +51,7 @@
Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML basis.ML \
codegen.ML context.ML display.ML drule.ML envir.ML goals.ML \
install_pp.ML library.ML logic.ML meta_simplifier.ML net.ML \
- pattern.ML proofterm.ML pure.ML pure_thy.ML search.ML sign.ML \
+ pattern.ML proof_general.ML proofterm.ML pure.ML pure_thy.ML search.ML sign.ML \
sorts.ML tactic.ML tctical.ML term.ML theory.ML theory_data.ML \
thm.ML type.ML type_infer.ML unify.ML
@./mk
--- a/src/Pure/ROOT.ML Wed Jan 16 17:53:22 2002 +0100
+++ b/src/Pure/ROOT.ML Wed Jan 16 20:57:02 2002 +0100
@@ -64,8 +64,8 @@
(*old-style goal package*)
use "goals.ML";
-(*specific support for user-interfaces*)
-cd "Interface"; use "ROOT.ML"; cd "..";
+(*configuration for Proof General*)
+use "proof_general.ML";
(*final Pure theory setup*)
use "pure.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/proof_general.ML Wed Jan 16 20:57:02 2002 +0100
@@ -0,0 +1,364 @@
+(* Title: Pure/Interface/proof_general.ML
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+Isabelle configuration for Proof General (see http://www.proofgeneral.org).
+*)
+
+signature PROOF_GENERAL =
+sig
+ val setup: (theory -> theory) list
+ val update_thy_only: string -> unit
+ val try_update_thy_only: string -> unit
+ val inform_file_processed: string -> unit
+ val inform_file_retracted: string -> unit
+ val thms_containing: string list -> unit
+ val help: unit -> unit
+ val show_context: unit -> theory
+ val kill_goal: unit -> unit
+ val repeat_undo: int -> unit
+ val isa_restart: unit -> unit
+ val init: bool -> unit
+ val write_keywords: string -> unit
+end;
+
+structure ProofGeneral: PROOF_GENERAL =
+struct
+
+(* print modes *)
+
+val proof_generalN = "ProofGeneral";
+val xsymbolsN = "xsymbols";
+
+val pgmlN = "PGML";
+fun pgml () = pgmlN mem_string ! print_mode;
+
+
+(* text output *)
+
+local
+
+fun xsymbols_output s =
+ if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
+ let val syms = Symbol.explode s
+ in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end
+ else (s, real (size s));
+
+fun pgml_output (s, len) =
+ if pgml () then (XML.text s, len)
+ else (s, len);
+
+in
+
+fun setup_xsymbols_output () =
+ Symbol.add_mode proof_generalN (pgml_output o xsymbols_output, Symbol.default_indent);
+
+end;
+
+
+(* token translations *)
+
+local
+
+val end_tag = oct_char "350";
+val class_tag = ("class", oct_char "351");
+val tfree_tag = ("tfree", oct_char "352");
+val tvar_tag = ("tvar", oct_char "353");
+val free_tag = ("free", oct_char "354");
+val bound_tag = ("bound", oct_char "355");
+val var_tag = ("var", oct_char "356");
+val skolem_tag = ("skolem", oct_char "357");
+
+fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
+
+fun tagit (kind, bg_tag) x =
+ (if pgml () then xml_atom kind x else bg_tag ^ x ^ end_tag,
+ real (Symbol.length (Symbol.explode x)));
+
+fun free_or_skolem x =
+ (case try Syntax.dest_skolem x of
+ None => tagit free_tag x
+ | Some x' => tagit skolem_tag x');
+
+fun var_or_skolem s =
+ (case Syntax.read_var s of
+ Var ((x, i), _) =>
+ (case try Syntax.dest_skolem x of
+ None => tagit var_tag s
+ | Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
+ | _ => tagit var_tag s);
+
+val proof_general_trans =
+ Syntax.tokentrans_mode proof_generalN
+ [("class", tagit class_tag),
+ ("tfree", tagit tfree_tag),
+ ("tvar", tagit tvar_tag),
+ ("free", free_or_skolem),
+ ("bound", tagit bound_tag),
+ ("var", var_or_skolem)];
+
+in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
+
+
+
+(* messages and notification *)
+
+local
+
+fun decorated_output bg en prfx =
+ writeln_default o enclose bg en o prefix_lines prfx;
+
+fun message kind bg en prfx s =
+ if pgml () then writeln_default (XML.element kind [] [prefix_lines prfx s])
+ else decorated_output bg en prfx s;
+
+val notify = message "notify" (oct_char "360") (oct_char "361") "";
+
+in
+
+fun setup_messages () =
+ (writeln_fn := message "output" "" "" "";
+ priority_fn := message "information" (oct_char "360") (oct_char "361") "";
+ tracing_fn := message "tracing" (oct_char "360" ^ oct_char "375") (oct_char "361") "";
+ warning_fn := message "warning" (oct_char "362") (oct_char "363") "### ";
+ error_fn := message "error" (oct_char "364") (oct_char "365") "*** ");
+
+fun tell_clear_goals () = notify "Proof General, please clear the goals buffer.";
+fun tell_clear_response () = notify "Proof General, please clear the response buffer.";
+fun tell_file msg path = notify ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
+
+end;
+
+
+(* theory / proof state output *)
+
+local
+
+fun tmp_markers f =
+ setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f ();
+
+fun statedisplay prts =
+ writeln_default (XML.element "statedisplay" [] [Pretty.string_of (Pretty.chunks prts)]);
+
+fun print_current_goals n m st =
+ if pgml () then statedisplay (Display.pretty_current_goals n m st)
+ else tmp_markers (fn () => Display.print_current_goals_default n m st);
+
+fun print_state b st =
+ if pgml () then statedisplay (Toplevel.pretty_state b st)
+ else tmp_markers (fn () => Toplevel.print_state_default b st);
+
+in
+
+fun setup_state () =
+ (Display.print_current_goals_fn := print_current_goals;
+ Toplevel.print_state_fn := print_state;
+ Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
+
+end;
+
+
+(* theory loader actions *)
+
+local
+
+fun add_master_files name files =
+ let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
+ in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
+
+fun trace_action action name =
+ if action = ThyInfo.Update then
+ seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name)
+ else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
+ seq (tell_file "you can unlock the file") (add_master_files name (ThyInfo.loaded_files name))
+ else ();
+
+in
+ fun setup_thy_loader () = ThyInfo.add_hook trace_action;
+ fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
+end;
+
+
+(* prepare theory context *)
+
+val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
+val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
+
+fun which_context () =
+ (case Context.get_context () of
+ Some thy => " Using current (dynamic!) one: " ^
+ (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
+ | None => "");
+
+fun try_update_thy_only file =
+ ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
+ let val name = thy_name file in
+ if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name
+ else warning ("Unkown theory context of ML file." ^ which_context ())
+ end) ();
+
+
+(* get informed about files *)
+
+val touch_child_thys = ThyInfo.if_known_thy ThyInfo.touch_child_thys;
+
+val inform_file_processed = touch_child_thys o thy_name;
+val inform_file_retracted = touch_child_thys o thy_name;
+
+fun proper_inform_file_processed file state =
+ let val name = thy_name file in
+ touch_child_thys name;
+ if not (Toplevel.is_toplevel state) then
+ warning ("Not at toplevel -- cannot register theory " ^ quote name)
+ else Library.transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
+ (warning msg; warning ("Failed to register theory " ^ quote name))
+ end;
+
+
+(* misc commands for ProofGeneral/isa *)
+
+fun thms_containing ss =
+ let
+ val thy = the_context ();
+ fun read_term s = Thm.term_of (Thm.read_cterm (Theory.sign_of thy) (s, TypeInfer.logicT));
+ in ThmDatabase.print_thms_containing thy (map read_term ss) end;
+
+val welcome = priority o Session.welcome;
+val help = welcome;
+val show_context = Context.the_context;
+
+fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
+
+fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
+
+fun repeat_undo 0 = ()
+ | repeat_undo 1 = undo ()
+ | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
+
+
+(* restart top-level loop (keeps most state information) *)
+
+local
+
+fun restart isar =
+ (if isar then tell_clear_goals () else kill_goal ();
+ tell_clear_response ();
+ welcome ());
+
+in
+
+fun isa_restart () = restart false;
+fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
+
+end;
+
+
+(* outer syntax *)
+
+local structure P = OuterParse and K = OuterSyntax.Keyword in
+
+val old_undoP = (*same name for compatibility with PG/Isabelle99*)
+ OuterSyntax.improper_command "undo" "undo last command (no output)" K.control
+ (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
+
+val undoP =
+ OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
+ (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
+
+val context_thy_onlyP =
+ OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
+ (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
+
+val try_context_thy_onlyP =
+ OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
+ (P.name >> (Toplevel.no_timing oo
+ (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
+
+val restartP =
+ OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
+ (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
+
+val kill_proofP =
+ OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
+ (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
+
+val inform_file_processedP =
+ OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
+ (P.name >> (Toplevel.no_timing oo
+ (fn name => Toplevel.keep (proper_inform_file_processed name))));
+
+val inform_file_retractedP =
+ OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
+ (P.name >> (Toplevel.no_timing oo
+ (fn name => Toplevel.imperative (fn () => inform_file_retracted name))));
+
+fun init_outer_syntax () = OuterSyntax.add_parsers
+ [old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
+ inform_file_processedP, inform_file_retractedP];
+
+end;
+
+
+(* init *)
+
+val initialized = ref false;
+
+fun init isar =
+ (conditional (not (! initialized)) (fn () =>
+ (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
+ setup_xsymbols_output ();
+ setup_messages ();
+ setup_state ();
+ setup_thy_loader ();
+ set initialized; ()));
+ sync_thy_loader ();
+ print_mode := proof_generalN :: (! print_mode \ proof_generalN);
+ set quick_and_dirty;
+ ThmDeps.enable ();
+ if isar then ml_prompts "ML> " "ML# "
+ else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
+ if isar then (welcome (); Isar.sync_main ()) else isa_restart ());
+
+
+
+(** generate keyword classification file **)
+
+local
+
+val regexp_meta = explode ".*+?[]^$";
+val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
+
+fun defconst name strs =
+ "\n(defconst isar-keywords-" ^ name ^
+ "\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n";
+
+fun make_elisp_commands commands kind =
+ defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
+
+fun make_elisp_syntax (keywords, commands) =
+ ";;\n\
+ \;; Keyword classification tables for Isabelle/Isar.\n\
+ \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
+ \;;\n\
+ \;; $" ^ "Id$\n\
+ \;;\n" ^
+ defconst "major" (map #1 commands) ^
+ defconst "minor" (filter Syntax.is_identifier keywords) ^
+ implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
+ "\n(provide 'isar-keywords)\n";
+
+in
+
+fun write_keywords s =
+ (init_outer_syntax ();
+ File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
+ (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
+
+end;
+
+
+end;
+
+(*a hack for Proof General 3.2 to avoid problems with escapes in ML commands*)
+infix \\\\ val op \\\\ = op \\;