src/Pure/Interface/proof_general.ML
changeset 7193 cc7a89d233f7
parent 7100 4f777a0e1c8b
child 7195 a38dc0c6b244
equal deleted inserted replaced
7192:30a67acd0d7e 7193:cc7a89d233f7
     7 
     7 
     8 signature PROOF_GENERAL =
     8 signature PROOF_GENERAL =
     9 sig
     9 sig
    10   val write_keywords: unit -> unit
    10   val write_keywords: unit -> unit
    11   val setup: (theory -> theory) list
    11   val setup: (theory -> theory) list
       
    12   val help: unit -> unit
       
    13   val show_context: unit -> theory
       
    14   val kill_goal: unit -> unit
       
    15   val repeat_undo: int -> unit
    12   val init: bool -> unit
    16   val init: bool -> unit
       
    17   val isa_restart: unit -> unit
    13 end;
    18 end;
    14 
    19 
    15 structure ProofGeneral: PROOF_GENERAL =
    20 structure ProofGeneral: PROOF_GENERAL =
    16 struct
    21 struct
    17 
    22 
    89 
    94 
    90 val setup = [Theory.add_tokentrfuns proof_general_trans];
    95 val setup = [Theory.add_tokentrfuns proof_general_trans];
    91 
    96 
    92 
    97 
    93 
    98 
    94 (** run-time initialization **)
    99 (** run-time operations **)
    95 
   100 
    96 (* messages *)
   101 (* messages *)
    97 
   102 
    98 fun decorate_lines bg en "" = std_output o suffix "\n" o enclose bg en
   103 val plain_output = std_output o suffix "\n";
    99   | decorate_lines bg en prfx = std_output o suffix "\n" o enclose bg en o prefix_lines prfx;
   104 val plain_writeln = Library.setmp writeln_fn plain_output;
       
   105 
       
   106 fun decorate_lines bg en "" = plain_output o enclose bg en
       
   107   | decorate_lines bg en prfx = plain_output o enclose bg en o prefix_lines prfx;
   100 
   108 
   101 fun setup_messages () =
   109 fun setup_messages () =
   102  (writeln_fn := (decorate_lines (oct_char "360") (oct_char "361") "");
   110  (writeln_fn := (decorate_lines (oct_char "360") (oct_char "361") "");
   103   warning_fn := (decorate_lines (oct_char "362") (oct_char "363") "### ");
   111   warning_fn := (decorate_lines (oct_char "362") (oct_char "363") "### ");
   104   error_fn := (decorate_lines (oct_char "364") (oct_char "365") "*** "));
   112   error_fn := (decorate_lines (oct_char "364") (oct_char "365") "*** "));
   105 
   113 
   106 
   114 
   107 (* theory / proof state *)
   115 (* theory / proof state *)
   108 
   116 
   109 fun setup_state () =
   117 fun print_current_goals n max th = plain_writeln (Goals.print_current_goals_default n max) th;
       
   118 
       
   119 fun setup_state isar =
   110   (current_goals_markers :=
   120   (current_goals_markers :=
   111     let
   121     let
   112       val begin_state = oct_char "366";
   122       val begin_state = oct_char "366";
   113       val end_state= oct_char "367";
   123       val end_state= oct_char "367";
   114       val begin_goal = oct_char "370";
   124       val begin_goal = oct_char "370";
   115     in (begin_state, end_state, begin_goal) end;
   125     in (begin_state, end_state, begin_goal) end;
   116   Toplevel.print_state_fn :=
   126   if isar then
   117     (Library.setmp writeln_fn (std_output o suffix "\n") Toplevel.print_state_default);
   127    (Toplevel.print_state_fn := plain_writeln Toplevel.print_state_default;
   118   Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
   128     Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default))
       
   129   else Goals.print_current_goals_fn := print_current_goals);
   119 
   130 
   120 
   131 
   121 (* theory loader actions *)
   132 (* theory loader actions *)
   122 
   133 
   123 local
   134 local
   124 
   135 
   125 fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
   136 fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
   126 
   137 
   127 fun trace_action ThyInfo.Update name = tell_pg "this theory is loaded:" name
   138 fun isa_action action name =
   128   | trace_action ThyInfo.Outdate name = tell_pg "you can unlock the theory" name
   139   let val files = map (File.sysify_path o #1) (ThyInfo.loaded_files name) in
   129   | trace_action ThyInfo.Remove name = tell_pg "you can unlock the theory" name;
   140     if action = ThyInfo.Update then seq (tell_pg "this file is loaded:") files
       
   141     else seq (tell_pg "you can unlock the file") files
       
   142   end;
       
   143 
       
   144 fun isar_action action name =
       
   145   if action = ThyInfo.Update then tell_pg "this theory is loaded:" name
       
   146   else tell_pg "you can unlock the theory" name;
   130 
   147 
   131 in
   148 in
   132   fun setup_thy_loader () = ThyInfo.add_hook trace_action;
   149   fun setup_thy_loader isar = ThyInfo.add_hook (if isar then isar_action else isa_action);
   133 end;
   150 end;
       
   151 
       
   152 
       
   153 (* some top-level commands for ProofGeneral/isa *)
       
   154 
       
   155 val help = writeln o Session.welcome;
       
   156 val show_context = Context.the_context;
       
   157 
       
   158 fun kill_goal () =
       
   159   (Goal "PROP no_goal_supplied"; writeln ("Proof General, please clear the goals buffer."));
       
   160 
       
   161 fun repeat_undo 0 = ()
       
   162   | repeat_undo n = (undo(); repeat_undo (n - 1));
       
   163 
       
   164 
       
   165 fun isa_restart () =
       
   166  (ml_prompts (">" ^ oct_char "372") ("-" ^ oct_char "373");
       
   167   ThyInfo.touch_all_thys ();
       
   168   kill_goal ();
       
   169   writeln ("Proof General, please clear the response buffer.");
       
   170   writeln "Isabelle Proof General: Isabelle process ready!");
   134 
   171 
   135 
   172 
   136 (* init *)
   173 (* init *)
   137 
   174 
   138 fun init isar =
   175 fun init isar =
   139  (setup_messages ();
   176  (setup_messages ();
   140   setup_state ();
   177   setup_state isar;
   141   setup_thy_loader ();
   178   setup_thy_loader isar;
   142   print_mode := [proof_generalN];
   179   print_mode := [proof_generalN];
   143   set quick_and_dirty;
   180   set quick_and_dirty;
   144   if isar then Isar.sync_main () else ());
   181   if isar then Isar.sync_main () else isa_restart ());
   145 
   182 
   146 
   183 
   147 end;
   184 end;