(* Title: Pure/Interface/proof_general.ML
ID: $Id$
Author: Markus Wenzel, TU Muenchen
Configuration for Proof General of LFCS Edinburgh.
*)
signature PROOF_GENERAL =
sig
val write_keywords: unit -> unit
val setup: (theory -> theory) list
val thms_containing: xstring 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
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 *)
val proof_generalN = "ProofGeneral";
local
val end_tag = oct_char "350";
val tclass_tag = oct_char "351";
val tfree_tag = oct_char "352";
val tvar_tag = oct_char "353";
val free_tag = oct_char "354";
val bound_tag = oct_char "355";
val var_tag = oct_char "356";
val skolem_tag = oct_char "357";
fun tagit p x = (p ^ x ^ end_tag, real (size x));
fun free_or_skolem x =
(case try Syntax.dest_skolem x of
None => tagit free_tag x
| Some x' => tagit skolem_tag x');
in
val proof_general_trans =
Syntax.tokentrans_mode proof_generalN
[("class", tagit tclass_tag),
("tfree", tagit tfree_tag),
("tvar", tagit tvar_tag),
("free", free_or_skolem),
("bound", tagit bound_tag),
("var", tagit var_tag)];
end;
(* setup *)
val setup = [Theory.add_tokentrfuns proof_general_trans];
(** run-time operations **)
(* messages *)
val plain_output = std_output o suffix "\n";
fun plain_writeln x = Library.setmp writeln_fn plain_output x;
fun decorate_lines bg en "" = plain_output o enclose bg en
| decorate_lines bg en prfx = plain_output o enclose bg en o prefix_lines prfx;
fun setup_messages () =
(writeln_fn := (decorate_lines (oct_char "360") (oct_char "361") "");
warning_fn := (decorate_lines (oct_char "362") (oct_char "363") "### ");
error_fn := (decorate_lines (oct_char "364") (oct_char "365") "*** "));
(* theory / proof state *)
fun print_current_goals n max th = plain_writeln (Goals.print_current_goals_default n max) th;
fun setup_state isar =
(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;
if isar then
(Toplevel.print_state_fn := plain_writeln Toplevel.print_state_default;
Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default))
else ();
Goals.print_current_goals_fn := print_current_goals); (*isar: avoids verbose responses*)
(* theory loader actions *)
local
fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
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;
in
fun setup_thy_loader () = ThyInfo.add_hook trace_action;
end;
(* some top-level 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 repeat_undo 0 = ()
| repeat_undo n = (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!");
(* init *)
fun init isar =
(setup_messages ();
setup_state isar;
setup_thy_loader ();
print_mode := [proof_generalN];
set quick_and_dirty;
if isar then Isar.sync_main () else isa_restart ());
end;