Interface/proof_general.ML move to proof_general.ML;
authorwenzelm
Wed Jan 16 20:57:02 2002 +0100 (2002-01-16)
changeset 127783120e338ffae
parent 12777 70b2651af635
child 12779 c5739c1431ab
Interface/proof_general.ML move to proof_general.ML;
src/Pure/Interface/ROOT.ML
src/Pure/Interface/proof_general.ML
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/Interface/ROOT.ML	Wed Jan 16 17:53:22 2002 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,7 +0,0 @@
     1.4 -(*  Title:      Pure/Interface/ROOT.ML
     1.5 -    ID:         $Id$
     1.6 -
     1.7 -Specific support for user-interfaces.
     1.8 -*)
     1.9 -
    1.10 -use "proof_general.ML";
     2.1 --- a/src/Pure/Interface/proof_general.ML	Wed Jan 16 17:53:22 2002 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,364 +0,0 @@
     2.4 -(*  Title:      Pure/Interface/proof_general.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Markus Wenzel, TU Muenchen
     2.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8 -
     2.9 -Isabelle configuration for Proof General (see http://www.proofgeneral.org).
    2.10 -*)
    2.11 -
    2.12 -signature PROOF_GENERAL =
    2.13 -sig
    2.14 -  val setup: (theory -> theory) list
    2.15 -  val update_thy_only: string -> unit
    2.16 -  val try_update_thy_only: string -> unit
    2.17 -  val inform_file_processed: string -> unit
    2.18 -  val inform_file_retracted: string -> unit
    2.19 -  val thms_containing: string list -> unit
    2.20 -  val help: unit -> unit
    2.21 -  val show_context: unit -> theory
    2.22 -  val kill_goal: unit -> unit
    2.23 -  val repeat_undo: int -> unit
    2.24 -  val isa_restart: unit -> unit
    2.25 -  val init: bool -> unit
    2.26 -  val write_keywords: string -> unit
    2.27 -end;
    2.28 -
    2.29 -structure ProofGeneral: PROOF_GENERAL =
    2.30 -struct
    2.31 -
    2.32 -(* print modes *)
    2.33 -
    2.34 -val proof_generalN = "ProofGeneral";
    2.35 -val xsymbolsN = "xsymbols";
    2.36 -
    2.37 -val pgmlN = "PGML";
    2.38 -fun pgml () = pgmlN mem_string ! print_mode;
    2.39 -
    2.40 -
    2.41 -(* text output *)
    2.42 -
    2.43 -local
    2.44 -
    2.45 -fun xsymbols_output s =
    2.46 -  if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
    2.47 -    let val syms = Symbol.explode s
    2.48 -    in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end
    2.49 -  else (s, real (size s));
    2.50 -
    2.51 -fun pgml_output (s, len) =
    2.52 -  if pgml () then (XML.text s, len)
    2.53 -  else (s, len);
    2.54 -
    2.55 -in
    2.56 -
    2.57 -fun setup_xsymbols_output () =
    2.58 -  Symbol.add_mode proof_generalN (pgml_output o xsymbols_output, Symbol.default_indent);
    2.59 -
    2.60 -end;
    2.61 -
    2.62 -
    2.63 -(* token translations *)
    2.64 -
    2.65 -local
    2.66 -
    2.67 -val end_tag = oct_char "350";
    2.68 -val class_tag = ("class", oct_char "351");
    2.69 -val tfree_tag = ("tfree", oct_char "352");
    2.70 -val tvar_tag = ("tvar", oct_char "353");
    2.71 -val free_tag = ("free", oct_char "354");
    2.72 -val bound_tag = ("bound", oct_char "355");
    2.73 -val var_tag = ("var", oct_char "356");
    2.74 -val skolem_tag = ("skolem", oct_char "357");
    2.75 -
    2.76 -fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
    2.77 -
    2.78 -fun tagit (kind, bg_tag) x =
    2.79 -  (if pgml () then xml_atom kind x else bg_tag ^ x ^ end_tag,
    2.80 -    real (Symbol.length (Symbol.explode x)));
    2.81 -
    2.82 -fun free_or_skolem x =
    2.83 -  (case try Syntax.dest_skolem x of
    2.84 -    None => tagit free_tag x
    2.85 -  | Some x' => tagit skolem_tag x');
    2.86 -
    2.87 -fun var_or_skolem s =
    2.88 -  (case Syntax.read_var s of
    2.89 -    Var ((x, i), _) =>
    2.90 -      (case try Syntax.dest_skolem x of
    2.91 -        None => tagit var_tag s
    2.92 -      | Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
    2.93 -  | _ => tagit var_tag s);
    2.94 -
    2.95 -val proof_general_trans =
    2.96 - Syntax.tokentrans_mode proof_generalN
    2.97 -  [("class", tagit class_tag),
    2.98 -   ("tfree", tagit tfree_tag),
    2.99 -   ("tvar", tagit tvar_tag),
   2.100 -   ("free", free_or_skolem),
   2.101 -   ("bound", tagit bound_tag),
   2.102 -   ("var", var_or_skolem)];
   2.103 -
   2.104 -in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
   2.105 -
   2.106 -
   2.107 -
   2.108 -(* messages and notification *)
   2.109 -
   2.110 -local
   2.111 -
   2.112 -fun decorated_output bg en prfx =
   2.113 -  writeln_default o enclose bg en o prefix_lines prfx;
   2.114 -
   2.115 -fun message kind bg en prfx s =
   2.116 -  if pgml () then writeln_default (XML.element kind [] [prefix_lines prfx s])
   2.117 -  else decorated_output bg en prfx s;
   2.118 -
   2.119 -val notify = message "notify" (oct_char "360") (oct_char "361") "";
   2.120 -
   2.121 -in
   2.122 -
   2.123 -fun setup_messages () =
   2.124 - (writeln_fn := message "output" "" "" "";
   2.125 -  priority_fn := message "information" (oct_char "360") (oct_char "361") "";
   2.126 -  tracing_fn := message "tracing" (oct_char "360" ^ oct_char "375") (oct_char "361") "";
   2.127 -  warning_fn := message "warning" (oct_char "362") (oct_char "363") "### ";
   2.128 -  error_fn := message "error" (oct_char "364") (oct_char "365") "*** ");
   2.129 -
   2.130 -fun tell_clear_goals () = notify "Proof General, please clear the goals buffer.";
   2.131 -fun tell_clear_response () = notify "Proof General, please clear the response buffer.";
   2.132 -fun tell_file msg path = notify ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
   2.133 -
   2.134 -end;
   2.135 -
   2.136 -
   2.137 -(* theory / proof state output *)
   2.138 -
   2.139 -local
   2.140 -
   2.141 -fun tmp_markers f =
   2.142 -  setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f ();
   2.143 -
   2.144 -fun statedisplay prts =
   2.145 -  writeln_default (XML.element "statedisplay" [] [Pretty.string_of (Pretty.chunks prts)]);
   2.146 -
   2.147 -fun print_current_goals n m st =
   2.148 -  if pgml () then statedisplay (Display.pretty_current_goals n m st)
   2.149 -  else tmp_markers (fn () => Display.print_current_goals_default n m st);
   2.150 -
   2.151 -fun print_state b st =
   2.152 -  if pgml () then statedisplay (Toplevel.pretty_state b st)
   2.153 -  else tmp_markers (fn () => Toplevel.print_state_default b st);
   2.154 -
   2.155 -in
   2.156 -
   2.157 -fun setup_state () =
   2.158 - (Display.print_current_goals_fn := print_current_goals;
   2.159 -  Toplevel.print_state_fn := print_state;
   2.160 -  Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
   2.161 -
   2.162 -end;
   2.163 -
   2.164 -
   2.165 -(* theory loader actions *)
   2.166 -
   2.167 -local
   2.168 -
   2.169 -fun add_master_files name files =
   2.170 -  let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
   2.171 -  in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
   2.172 -
   2.173 -fun trace_action action name =
   2.174 -  if action = ThyInfo.Update then
   2.175 -    seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name)
   2.176 -  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
   2.177 -    seq (tell_file "you can unlock the file") (add_master_files name (ThyInfo.loaded_files name))
   2.178 -  else ();
   2.179 -
   2.180 -in
   2.181 -  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
   2.182 -  fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
   2.183 -end;
   2.184 -
   2.185 -
   2.186 -(* prepare theory context *)
   2.187 -
   2.188 -val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
   2.189 -val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
   2.190 -
   2.191 -fun which_context () =
   2.192 -  (case Context.get_context () of
   2.193 -    Some thy => "  Using current (dynamic!) one: " ^
   2.194 -      (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
   2.195 -  | None => "");
   2.196 -
   2.197 -fun try_update_thy_only file =
   2.198 -  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
   2.199 -    let val name = thy_name file in
   2.200 -      if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name
   2.201 -      else warning ("Unkown theory context of ML file." ^ which_context ())
   2.202 -    end) ();
   2.203 -
   2.204 -
   2.205 -(* get informed about files *)
   2.206 -
   2.207 -val touch_child_thys = ThyInfo.if_known_thy ThyInfo.touch_child_thys;
   2.208 -
   2.209 -val inform_file_processed = touch_child_thys o thy_name;
   2.210 -val inform_file_retracted = touch_child_thys o thy_name;
   2.211 -
   2.212 -fun proper_inform_file_processed file state =
   2.213 -  let val name = thy_name file in
   2.214 -    touch_child_thys name;
   2.215 -    if not (Toplevel.is_toplevel state) then
   2.216 -      warning ("Not at toplevel -- cannot register theory " ^ quote name)
   2.217 -    else Library.transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
   2.218 -      (warning msg; warning ("Failed to register theory " ^ quote name))
   2.219 -  end;
   2.220 -
   2.221 -
   2.222 -(* misc commands for ProofGeneral/isa *)
   2.223 -
   2.224 -fun thms_containing ss =
   2.225 -  let
   2.226 -    val thy = the_context ();
   2.227 -    fun read_term s = Thm.term_of (Thm.read_cterm (Theory.sign_of thy) (s, TypeInfer.logicT));
   2.228 -  in ThmDatabase.print_thms_containing thy (map read_term ss) end;
   2.229 -
   2.230 -val welcome = priority o Session.welcome;
   2.231 -val help = welcome;
   2.232 -val show_context = Context.the_context;
   2.233 -
   2.234 -fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
   2.235 -
   2.236 -fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
   2.237 -
   2.238 -fun repeat_undo 0 = ()
   2.239 -  | repeat_undo 1 = undo ()
   2.240 -  | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
   2.241 -
   2.242 -
   2.243 -(* restart top-level loop (keeps most state information) *)
   2.244 -
   2.245 -local
   2.246 -
   2.247 -fun restart isar =
   2.248 - (if isar then tell_clear_goals () else kill_goal ();
   2.249 -  tell_clear_response ();
   2.250 -  welcome ());
   2.251 -
   2.252 -in
   2.253 -
   2.254 -fun isa_restart () = restart false;
   2.255 -fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
   2.256 -
   2.257 -end;
   2.258 -
   2.259 -
   2.260 -(* outer syntax *)
   2.261 -
   2.262 -local structure P = OuterParse and K = OuterSyntax.Keyword in
   2.263 -
   2.264 -val old_undoP = (*same name for compatibility with PG/Isabelle99*)
   2.265 -  OuterSyntax.improper_command "undo" "undo last command (no output)" K.control
   2.266 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
   2.267 -
   2.268 -val undoP =
   2.269 -  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
   2.270 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
   2.271 -
   2.272 -val context_thy_onlyP =
   2.273 -  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
   2.274 -    (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
   2.275 -
   2.276 -val try_context_thy_onlyP =
   2.277 -  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
   2.278 -    (P.name >> (Toplevel.no_timing oo
   2.279 -      (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
   2.280 -
   2.281 -val restartP =
   2.282 -  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
   2.283 -    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
   2.284 -
   2.285 -val kill_proofP =
   2.286 -  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
   2.287 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
   2.288 -
   2.289 -val inform_file_processedP =
   2.290 -  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
   2.291 -    (P.name >> (Toplevel.no_timing oo
   2.292 -      (fn name => Toplevel.keep (proper_inform_file_processed name))));
   2.293 -
   2.294 -val inform_file_retractedP =
   2.295 -  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
   2.296 -    (P.name >> (Toplevel.no_timing oo
   2.297 -      (fn name => Toplevel.imperative (fn () => inform_file_retracted name))));
   2.298 -
   2.299 -fun init_outer_syntax () = OuterSyntax.add_parsers
   2.300 - [old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
   2.301 -  inform_file_processedP, inform_file_retractedP];
   2.302 -
   2.303 -end;
   2.304 -
   2.305 -
   2.306 -(* init *)
   2.307 -
   2.308 -val initialized = ref false;
   2.309 -
   2.310 -fun init isar =
   2.311 - (conditional (not (! initialized)) (fn () =>
   2.312 -   (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
   2.313 -    setup_xsymbols_output ();
   2.314 -    setup_messages ();
   2.315 -    setup_state ();
   2.316 -    setup_thy_loader ();
   2.317 -    set initialized; ()));
   2.318 -  sync_thy_loader ();
   2.319 -  print_mode := proof_generalN :: (! print_mode \ proof_generalN);
   2.320 -  set quick_and_dirty;
   2.321 -  ThmDeps.enable ();
   2.322 -  if isar then ml_prompts "ML> " "ML# "
   2.323 -  else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
   2.324 -  if isar then (welcome (); Isar.sync_main ()) else isa_restart ());
   2.325 -
   2.326 -
   2.327 -
   2.328 -(** generate keyword classification file **)
   2.329 -
   2.330 -local
   2.331 -
   2.332 -val regexp_meta = explode ".*+?[]^$";
   2.333 -val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
   2.334 -
   2.335 -fun defconst name strs =
   2.336 -  "\n(defconst isar-keywords-" ^ name ^
   2.337 -  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
   2.338 -
   2.339 -fun make_elisp_commands commands kind =
   2.340 -  defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
   2.341 -
   2.342 -fun make_elisp_syntax (keywords, commands) =
   2.343 -  ";;\n\
   2.344 -  \;; Keyword classification tables for Isabelle/Isar.\n\
   2.345 -  \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
   2.346 -  \;;\n\
   2.347 -  \;; $" ^ "Id$\n\
   2.348 -  \;;\n" ^
   2.349 -  defconst "major" (map #1 commands) ^
   2.350 -  defconst "minor" (filter Syntax.is_identifier keywords) ^
   2.351 -  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
   2.352 -  "\n(provide 'isar-keywords)\n";
   2.353 -
   2.354 -in
   2.355 -
   2.356 -fun write_keywords s =
   2.357 -  (init_outer_syntax ();
   2.358 -    File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
   2.359 -      (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
   2.360 -
   2.361 -end;
   2.362 -
   2.363 -
   2.364 -end;
   2.365 -
   2.366 -(*a hack for Proof General 3.2 to avoid problems with escapes in ML commands*)
   2.367 -infix \\\\ val op \\\\ = op \\;
     3.1 --- a/src/Pure/IsaMakefile	Wed Jan 16 17:53:22 2002 +0100
     3.2 +++ b/src/Pure/IsaMakefile	Wed Jan 16 20:57:02 2002 +0100
     3.3 @@ -28,7 +28,7 @@
     3.4    General/name_space.ML General/object.ML General/path.ML		\
     3.5    General/position.ML General/pretty.ML General/scan.ML General/seq.ML	\
     3.6    General/source.ML General/symbol.ML General/table.ML General/url.ML	\
     3.7 -  General/xml.ML Interface/ROOT.ML Interface/proof_general.ML		\
     3.8 +  General/xml.ML 		\
     3.9    Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML		\
    3.10    Isar/auto_bind.ML Isar/calculation.ML Isar/comment.ML			\
    3.11    Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML		\
    3.12 @@ -51,7 +51,7 @@
    3.13    Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML basis.ML	\
    3.14    codegen.ML context.ML display.ML drule.ML envir.ML goals.ML		\
    3.15    install_pp.ML library.ML logic.ML meta_simplifier.ML net.ML		\
    3.16 -  pattern.ML proofterm.ML pure.ML pure_thy.ML search.ML sign.ML		\
    3.17 +  pattern.ML proof_general.ML proofterm.ML pure.ML pure_thy.ML search.ML sign.ML		\
    3.18    sorts.ML tactic.ML tctical.ML term.ML theory.ML theory_data.ML	\
    3.19    thm.ML type.ML type_infer.ML unify.ML
    3.20  	@./mk
     4.1 --- a/src/Pure/ROOT.ML	Wed Jan 16 17:53:22 2002 +0100
     4.2 +++ b/src/Pure/ROOT.ML	Wed Jan 16 20:57:02 2002 +0100
     4.3 @@ -64,8 +64,8 @@
     4.4  (*old-style goal package*)
     4.5  use "goals.ML";
     4.6  
     4.7 -(*specific support for user-interfaces*)
     4.8 -cd "Interface"; use "ROOT.ML"; cd "..";
     4.9 +(*configuration for Proof General*)
    4.10 +use "proof_general.ML";
    4.11  
    4.12  (*final Pure theory setup*)
    4.13  use "pure.ML";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/proof_general.ML	Wed Jan 16 20:57:02 2002 +0100
     5.3 @@ -0,0 +1,364 @@
     5.4 +(*  Title:      Pure/Interface/proof_general.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Markus Wenzel, TU Muenchen
     5.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5.8 +
     5.9 +Isabelle configuration for Proof General (see http://www.proofgeneral.org).
    5.10 +*)
    5.11 +
    5.12 +signature PROOF_GENERAL =
    5.13 +sig
    5.14 +  val setup: (theory -> theory) list
    5.15 +  val update_thy_only: string -> unit
    5.16 +  val try_update_thy_only: string -> unit
    5.17 +  val inform_file_processed: string -> unit
    5.18 +  val inform_file_retracted: string -> unit
    5.19 +  val thms_containing: string list -> unit
    5.20 +  val help: unit -> unit
    5.21 +  val show_context: unit -> theory
    5.22 +  val kill_goal: unit -> unit
    5.23 +  val repeat_undo: int -> unit
    5.24 +  val isa_restart: unit -> unit
    5.25 +  val init: bool -> unit
    5.26 +  val write_keywords: string -> unit
    5.27 +end;
    5.28 +
    5.29 +structure ProofGeneral: PROOF_GENERAL =
    5.30 +struct
    5.31 +
    5.32 +(* print modes *)
    5.33 +
    5.34 +val proof_generalN = "ProofGeneral";
    5.35 +val xsymbolsN = "xsymbols";
    5.36 +
    5.37 +val pgmlN = "PGML";
    5.38 +fun pgml () = pgmlN mem_string ! print_mode;
    5.39 +
    5.40 +
    5.41 +(* text output *)
    5.42 +
    5.43 +local
    5.44 +
    5.45 +fun xsymbols_output s =
    5.46 +  if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
    5.47 +    let val syms = Symbol.explode s
    5.48 +    in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end
    5.49 +  else (s, real (size s));
    5.50 +
    5.51 +fun pgml_output (s, len) =
    5.52 +  if pgml () then (XML.text s, len)
    5.53 +  else (s, len);
    5.54 +
    5.55 +in
    5.56 +
    5.57 +fun setup_xsymbols_output () =
    5.58 +  Symbol.add_mode proof_generalN (pgml_output o xsymbols_output, Symbol.default_indent);
    5.59 +
    5.60 +end;
    5.61 +
    5.62 +
    5.63 +(* token translations *)
    5.64 +
    5.65 +local
    5.66 +
    5.67 +val end_tag = oct_char "350";
    5.68 +val class_tag = ("class", oct_char "351");
    5.69 +val tfree_tag = ("tfree", oct_char "352");
    5.70 +val tvar_tag = ("tvar", oct_char "353");
    5.71 +val free_tag = ("free", oct_char "354");
    5.72 +val bound_tag = ("bound", oct_char "355");
    5.73 +val var_tag = ("var", oct_char "356");
    5.74 +val skolem_tag = ("skolem", oct_char "357");
    5.75 +
    5.76 +fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
    5.77 +
    5.78 +fun tagit (kind, bg_tag) x =
    5.79 +  (if pgml () then xml_atom kind x else bg_tag ^ x ^ end_tag,
    5.80 +    real (Symbol.length (Symbol.explode x)));
    5.81 +
    5.82 +fun free_or_skolem x =
    5.83 +  (case try Syntax.dest_skolem x of
    5.84 +    None => tagit free_tag x
    5.85 +  | Some x' => tagit skolem_tag x');
    5.86 +
    5.87 +fun var_or_skolem s =
    5.88 +  (case Syntax.read_var s of
    5.89 +    Var ((x, i), _) =>
    5.90 +      (case try Syntax.dest_skolem x of
    5.91 +        None => tagit var_tag s
    5.92 +      | Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
    5.93 +  | _ => tagit var_tag s);
    5.94 +
    5.95 +val proof_general_trans =
    5.96 + Syntax.tokentrans_mode proof_generalN
    5.97 +  [("class", tagit class_tag),
    5.98 +   ("tfree", tagit tfree_tag),
    5.99 +   ("tvar", tagit tvar_tag),
   5.100 +   ("free", free_or_skolem),
   5.101 +   ("bound", tagit bound_tag),
   5.102 +   ("var", var_or_skolem)];
   5.103 +
   5.104 +in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
   5.105 +
   5.106 +
   5.107 +
   5.108 +(* messages and notification *)
   5.109 +
   5.110 +local
   5.111 +
   5.112 +fun decorated_output bg en prfx =
   5.113 +  writeln_default o enclose bg en o prefix_lines prfx;
   5.114 +
   5.115 +fun message kind bg en prfx s =
   5.116 +  if pgml () then writeln_default (XML.element kind [] [prefix_lines prfx s])
   5.117 +  else decorated_output bg en prfx s;
   5.118 +
   5.119 +val notify = message "notify" (oct_char "360") (oct_char "361") "";
   5.120 +
   5.121 +in
   5.122 +
   5.123 +fun setup_messages () =
   5.124 + (writeln_fn := message "output" "" "" "";
   5.125 +  priority_fn := message "information" (oct_char "360") (oct_char "361") "";
   5.126 +  tracing_fn := message "tracing" (oct_char "360" ^ oct_char "375") (oct_char "361") "";
   5.127 +  warning_fn := message "warning" (oct_char "362") (oct_char "363") "### ";
   5.128 +  error_fn := message "error" (oct_char "364") (oct_char "365") "*** ");
   5.129 +
   5.130 +fun tell_clear_goals () = notify "Proof General, please clear the goals buffer.";
   5.131 +fun tell_clear_response () = notify "Proof General, please clear the response buffer.";
   5.132 +fun tell_file msg path = notify ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
   5.133 +
   5.134 +end;
   5.135 +
   5.136 +
   5.137 +(* theory / proof state output *)
   5.138 +
   5.139 +local
   5.140 +
   5.141 +fun tmp_markers f =
   5.142 +  setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f ();
   5.143 +
   5.144 +fun statedisplay prts =
   5.145 +  writeln_default (XML.element "statedisplay" [] [Pretty.string_of (Pretty.chunks prts)]);
   5.146 +
   5.147 +fun print_current_goals n m st =
   5.148 +  if pgml () then statedisplay (Display.pretty_current_goals n m st)
   5.149 +  else tmp_markers (fn () => Display.print_current_goals_default n m st);
   5.150 +
   5.151 +fun print_state b st =
   5.152 +  if pgml () then statedisplay (Toplevel.pretty_state b st)
   5.153 +  else tmp_markers (fn () => Toplevel.print_state_default b st);
   5.154 +
   5.155 +in
   5.156 +
   5.157 +fun setup_state () =
   5.158 + (Display.print_current_goals_fn := print_current_goals;
   5.159 +  Toplevel.print_state_fn := print_state;
   5.160 +  Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
   5.161 +
   5.162 +end;
   5.163 +
   5.164 +
   5.165 +(* theory loader actions *)
   5.166 +
   5.167 +local
   5.168 +
   5.169 +fun add_master_files name files =
   5.170 +  let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
   5.171 +  in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
   5.172 +
   5.173 +fun trace_action action name =
   5.174 +  if action = ThyInfo.Update then
   5.175 +    seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name)
   5.176 +  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
   5.177 +    seq (tell_file "you can unlock the file") (add_master_files name (ThyInfo.loaded_files name))
   5.178 +  else ();
   5.179 +
   5.180 +in
   5.181 +  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
   5.182 +  fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
   5.183 +end;
   5.184 +
   5.185 +
   5.186 +(* prepare theory context *)
   5.187 +
   5.188 +val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
   5.189 +val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
   5.190 +
   5.191 +fun which_context () =
   5.192 +  (case Context.get_context () of
   5.193 +    Some thy => "  Using current (dynamic!) one: " ^
   5.194 +      (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
   5.195 +  | None => "");
   5.196 +
   5.197 +fun try_update_thy_only file =
   5.198 +  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
   5.199 +    let val name = thy_name file in
   5.200 +      if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name
   5.201 +      else warning ("Unkown theory context of ML file." ^ which_context ())
   5.202 +    end) ();
   5.203 +
   5.204 +
   5.205 +(* get informed about files *)
   5.206 +
   5.207 +val touch_child_thys = ThyInfo.if_known_thy ThyInfo.touch_child_thys;
   5.208 +
   5.209 +val inform_file_processed = touch_child_thys o thy_name;
   5.210 +val inform_file_retracted = touch_child_thys o thy_name;
   5.211 +
   5.212 +fun proper_inform_file_processed file state =
   5.213 +  let val name = thy_name file in
   5.214 +    touch_child_thys name;
   5.215 +    if not (Toplevel.is_toplevel state) then
   5.216 +      warning ("Not at toplevel -- cannot register theory " ^ quote name)
   5.217 +    else Library.transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
   5.218 +      (warning msg; warning ("Failed to register theory " ^ quote name))
   5.219 +  end;
   5.220 +
   5.221 +
   5.222 +(* misc commands for ProofGeneral/isa *)
   5.223 +
   5.224 +fun thms_containing ss =
   5.225 +  let
   5.226 +    val thy = the_context ();
   5.227 +    fun read_term s = Thm.term_of (Thm.read_cterm (Theory.sign_of thy) (s, TypeInfer.logicT));
   5.228 +  in ThmDatabase.print_thms_containing thy (map read_term ss) end;
   5.229 +
   5.230 +val welcome = priority o Session.welcome;
   5.231 +val help = welcome;
   5.232 +val show_context = Context.the_context;
   5.233 +
   5.234 +fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
   5.235 +
   5.236 +fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
   5.237 +
   5.238 +fun repeat_undo 0 = ()
   5.239 +  | repeat_undo 1 = undo ()
   5.240 +  | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
   5.241 +
   5.242 +
   5.243 +(* restart top-level loop (keeps most state information) *)
   5.244 +
   5.245 +local
   5.246 +
   5.247 +fun restart isar =
   5.248 + (if isar then tell_clear_goals () else kill_goal ();
   5.249 +  tell_clear_response ();
   5.250 +  welcome ());
   5.251 +
   5.252 +in
   5.253 +
   5.254 +fun isa_restart () = restart false;
   5.255 +fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
   5.256 +
   5.257 +end;
   5.258 +
   5.259 +
   5.260 +(* outer syntax *)
   5.261 +
   5.262 +local structure P = OuterParse and K = OuterSyntax.Keyword in
   5.263 +
   5.264 +val old_undoP = (*same name for compatibility with PG/Isabelle99*)
   5.265 +  OuterSyntax.improper_command "undo" "undo last command (no output)" K.control
   5.266 +    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
   5.267 +
   5.268 +val undoP =
   5.269 +  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
   5.270 +    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
   5.271 +
   5.272 +val context_thy_onlyP =
   5.273 +  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
   5.274 +    (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
   5.275 +
   5.276 +val try_context_thy_onlyP =
   5.277 +  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
   5.278 +    (P.name >> (Toplevel.no_timing oo
   5.279 +      (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
   5.280 +
   5.281 +val restartP =
   5.282 +  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
   5.283 +    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
   5.284 +
   5.285 +val kill_proofP =
   5.286 +  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
   5.287 +    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
   5.288 +
   5.289 +val inform_file_processedP =
   5.290 +  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
   5.291 +    (P.name >> (Toplevel.no_timing oo
   5.292 +      (fn name => Toplevel.keep (proper_inform_file_processed name))));
   5.293 +
   5.294 +val inform_file_retractedP =
   5.295 +  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
   5.296 +    (P.name >> (Toplevel.no_timing oo
   5.297 +      (fn name => Toplevel.imperative (fn () => inform_file_retracted name))));
   5.298 +
   5.299 +fun init_outer_syntax () = OuterSyntax.add_parsers
   5.300 + [old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
   5.301 +  inform_file_processedP, inform_file_retractedP];
   5.302 +
   5.303 +end;
   5.304 +
   5.305 +
   5.306 +(* init *)
   5.307 +
   5.308 +val initialized = ref false;
   5.309 +
   5.310 +fun init isar =
   5.311 + (conditional (not (! initialized)) (fn () =>
   5.312 +   (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
   5.313 +    setup_xsymbols_output ();
   5.314 +    setup_messages ();
   5.315 +    setup_state ();
   5.316 +    setup_thy_loader ();
   5.317 +    set initialized; ()));
   5.318 +  sync_thy_loader ();
   5.319 +  print_mode := proof_generalN :: (! print_mode \ proof_generalN);
   5.320 +  set quick_and_dirty;
   5.321 +  ThmDeps.enable ();
   5.322 +  if isar then ml_prompts "ML> " "ML# "
   5.323 +  else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
   5.324 +  if isar then (welcome (); Isar.sync_main ()) else isa_restart ());
   5.325 +
   5.326 +
   5.327 +
   5.328 +(** generate keyword classification file **)
   5.329 +
   5.330 +local
   5.331 +
   5.332 +val regexp_meta = explode ".*+?[]^$";
   5.333 +val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
   5.334 +
   5.335 +fun defconst name strs =
   5.336 +  "\n(defconst isar-keywords-" ^ name ^
   5.337 +  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
   5.338 +
   5.339 +fun make_elisp_commands commands kind =
   5.340 +  defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
   5.341 +
   5.342 +fun make_elisp_syntax (keywords, commands) =
   5.343 +  ";;\n\
   5.344 +  \;; Keyword classification tables for Isabelle/Isar.\n\
   5.345 +  \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
   5.346 +  \;;\n\
   5.347 +  \;; $" ^ "Id$\n\
   5.348 +  \;;\n" ^
   5.349 +  defconst "major" (map #1 commands) ^
   5.350 +  defconst "minor" (filter Syntax.is_identifier keywords) ^
   5.351 +  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
   5.352 +  "\n(provide 'isar-keywords)\n";
   5.353 +
   5.354 +in
   5.355 +
   5.356 +fun write_keywords s =
   5.357 +  (init_outer_syntax ();
   5.358 +    File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
   5.359 +      (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
   5.360 +
   5.361 +end;
   5.362 +
   5.363 +
   5.364 +end;
   5.365 +
   5.366 +(*a hack for Proof General 3.2 to avoid problems with escapes in ML commands*)
   5.367 +infix \\\\ val op \\\\ = op \\;