# HG changeset patch # User wenzelm # Date 940957612 -7200 # Node ID 82025fe607d3b8b3c1dd00da54b342ffc0c3719a # Parent cbeaff0ef8562fd6be04c527a7a4098c71780e05 added inform_file_processed, inform_file_retracted; proper outer syntax setup; more robust theory loader actions; diff -r cbeaff0ef856 -r 82025fe607d3 src/Pure/Interface/proof_general.ML --- a/src/Pure/Interface/proof_general.ML Tue Oct 26 19:05:26 1999 +0200 +++ b/src/Pure/Interface/proof_general.ML Tue Oct 26 19:06:52 1999 +0200 @@ -7,7 +7,6 @@ signature PROOF_GENERAL = sig - val write_keywords: unit -> unit val setup: (theory -> theory) list val thms_containing: xstring list -> unit val help: unit -> unit @@ -15,50 +14,15 @@ val kill_goal: unit -> unit val repeat_undo: int -> unit val isa_restart: unit -> unit + val inform_file_processed: string -> unit + val inform_file_retracted: string -> unit val init: bool -> unit + val write_keywords: unit -> unit end; structure ProofGeneral: PROOF_GENERAL = struct - -(** 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 generated by Isabelle -- DO NOT EDIT!\n\ - \;;\n\ - \;; $" ^ "Id$\n\ - \;;\n" ^ - defconst "minor" (filter Syntax.is_identifier keywords) ^ - implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^ - "\n(provide 'isar-keywords)\n"; - -val keywords_file = "isar-keywords.el"; - -in - -fun write_keywords () = - File.write (Path.unpack keywords_file) - (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())); - -end; - - - (** compile-time theory setup **) (* token translations *) @@ -119,7 +83,14 @@ error_fn := (decorate_lines (oct_char "364") (oct_char "365") "*** ")); -(* theory / proof state *) +(* notification *) + +fun tell_clear_goals () = writeln "Proof General, please clear the goals buffer."; +fun tell_clear_response () = writeln "Proof General, please clear the response buffer."; +fun tell_file msg path = writeln ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path)); + + +(* theory / proof state output *) fun print_current_goals n max th = plain_writeln (Goals.print_current_goals_default n max) th; @@ -141,39 +112,42 @@ local -fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name); +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 = - let - val update = (action = ThyInfo.Update); - fun loaded (path, really) = - if update andalso not really then None - else Some path; - val tell = tell_pg (if update then "this file is loaded:" else "you can unlock the file") - o File.sysify_path; - - val (master, files) = ThyInfo.loaded_files name; - in - (case master of - Some path => tell path - | None => tell (ThyLoad.thy_path name)); (*just to make sure ...*) - seq tell (mapfilter loaded files) - end; + 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; end; -(* some top-level commands for ProofGeneral/isa *) +(* get informed about files *) + +val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack; + +(* FIXME improve, e.g. do something like pretend_use_thy *) +fun inform_file_processed file = + ThyInfo.if_known_thy ThyInfo.touch_child_thys (thy_name file); + +fun inform_file_retracted file = + ThyInfo.if_known_thy ThyInfo.touch_child_thys (thy_name file); + + +(* misc commands for ProofGeneral/isa *) fun thms_containing cs = ThmDatabase.print_thms_containing (the_context ()) cs; val help = writeln o Session.welcome; val show_context = Context.the_context; -fun kill_goal () = - (Goals.reset_goals (); writeln "Proof General, please clear the goals buffer."); +fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ()); fun no_print_goals f = setmp print_current_goals_fn (fn _ => fn _ => fn _ => ()) f; @@ -181,12 +155,49 @@ | repeat_undo 1 = undo () | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1)); -fun isa_restart () = - (ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373"); - ThyInfo.touch_all_thys (); - kill_goal (); - writeln "Proof General, please clear the response buffer."; - writeln "Isabelle Proof General: Isabelle process ready!"); + +(* re-init process (an approximation) *) + +local + +fun restart isar = + (ThyInfo.touch_all_thys (); + if isar then () else (ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373"); kill_goal ()); + tell_clear_response (); + writeln (Session.welcome ())); + +in + +fun isa_restart () = restart false; +fun isar_restart () = (restart true; raise Toplevel.RESTART); + +end; + + +(* outer syntax *) + +local structure P = OuterParse and K = OuterSyntax.Keyword in + +val restartP = + OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control + (P.opt_unit >> K (Toplevel.imperative isar_restart)); + +val kill_proofP = + OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control + (Scan.succeed (IsarCmd.kill_proof_notify tell_clear_goals)); + +val inform_file_processedP = + OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control + (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_processed name))); + +val inform_file_retractedP = + OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control + (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_retracted name))); + +fun init_outer_syntax () = + OuterSyntax.add_parsers [restartP, kill_proofP, inform_file_processedP, inform_file_retractedP]; + +end; (* init *) @@ -197,7 +208,46 @@ setup_thy_loader (); print_mode := [proof_generalN]; set quick_and_dirty; + if isar then init_outer_syntax () else (); if isar then 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 generated by Isabelle -- DO NOT EDIT!\n\ + \;;\n\ + \;; $" ^ "Id$\n\ + \;;\n" ^ + defconst "minor" (filter Syntax.is_identifier keywords) ^ + implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^ + "\n(provide 'isar-keywords)\n"; + +val keywords_file = "isar-keywords.el"; + +in + +fun write_keywords () = + (init_outer_syntax (); + File.write (Path.unpack keywords_file) + (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ()))); + end; + + +end;