src/Pure/Interface/proof_general.ML

Goals.reset_goals;

(*  Title:      Pure/Interface/proof_general.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Configuration for ProofGeneral of LFCS Edinburgh.
*)

signature PROOF_GENERAL =
sig
  val write_keywords: unit -> unit
  val setup: (theory -> theory) list
  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";

fun tagit p x = (p ^ x ^ end_tag, real (size x));

in

val proof_general_trans =
 Syntax.tokentrans_mode proof_generalN
  [("class", tagit tclass_tag),
   ("tfree", tagit tfree_tag),
   ("tvar", tagit tvar_tag),
   ("free", tagit free_tag),
   ("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);


(* theory loader actions *)

local

fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);

fun isa_action action name =
  let val files = map (File.sysify_path o #1) (ThyInfo.loaded_files name) in
    if action = ThyInfo.Update then seq (tell_pg "this file is loaded:") files
    else seq (tell_pg "you can unlock the file") files
  end;

fun isar_action action name =
  if action = ThyInfo.Update then tell_pg "this theory is loaded:" name
  else tell_pg "you can unlock the theory" name;

in
  fun setup_thy_loader isar = ThyInfo.add_hook (if isar then isar_action else isa_action);
end;


(* some top-level commands for ProofGeneral/isa *)

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 isar;
  print_mode := [proof_generalN];
  set quick_and_dirty;
  if isar then Isar.sync_main () else isa_restart ());


end;