Improvements and cleanups:

  . Put functions into ProofGeneral structure
  . Annotations around ordinary output appear before cr's
  . Added clear_response_buffer functionw
  . Added special_theories to avoid looking up filenames of
    theories which don't have them

1 files changed, 87 insertions, 167 deletions

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index 1986422d..96bbf66e 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -23,6 +23,10 @@ sig
    val retract_ML_file : string -> unit
    val retract_thy_file : string -> unit
    val repeat_undo : int -> unit
+   val clear_response_buffer : unit -> unit
+   val list_loaded_files : unit -> unit
+   val use_thy_and_update : string -> unit
+   val special_theories : string list ref
 end;
 
 structure ProofGeneral =
@@ -79,9 +83,47 @@ structure ProofGeneral =
 
    fun repeat_undo 0 = ()
      | repeat_undo n = (undo(); repeat_undo (n-1));
- end;
 
-fun remove_mlfile_fromdb thy =
+   fun clear_response_buffer () =
+      writeln("Proof General, please clear the response buffer.");
+
+   val special_theories = ref ["ProtoPure", "Pure", "CPure"];
+   
+   fun list_loaded_files () =
+   let
+     val thys_list = Symtab.dest (!loaded_thys)
+     fun loading_msg (tname,tinfo) =
+        if (tname mem (!special_theories)) then () else
+	 let val path = path_of tname
+	     val (thy_file,ml_file) = get_thy_filenames path tname
+	     fun file_msg x = if (x <> "") then
+			(* Simulate output of theory loader *)
+			writeln ("Reading " ^ (quote x))
+	               else ()
+	  in
+	     (file_msg thy_file; file_msg ml_file)
+          end
+   in
+    (writeln "Updating loaded files list...";
+     seq loading_msg thys_list)
+   end;
+
+ (* 
+   Possible alternative: parse "children are out of date"
+   message, and unlock those ones (plus descendants).
+   This seems feasible, but use_thy ought to do update
+   anyway, I think. 
+  *)
+
+  fun use_thy_and_update thy = 
+  (use_thy_no_topml thy;
+   update();
+   list_loaded_files();
+   clear_response_buffer());
+
+ end; (* struct ProofGeneral *)
+
+ fun remove_mlfile_fromdb thy =
   let val tinfo =  case Symtab.lookup (!loaded_thys, thy) of
 	Some ({path, children, parents = parents, thy_time, theory,...}) =>
 	{ path = path, children = children, parents = parents, theory=theory,
@@ -102,27 +144,6 @@ fun use_thy_and_update thy =
 *)
 
 
-
-fun list_loaded_files () =
- let
-   val thys_list = Symtab.dest (!loaded_thys)
-   fun loading_msg (tname,tinfo) = 
-	let val path = path_of tname
-	    val (thy_file,ml_file) = get_thy_filenames path tname
-	    fun file_msg x = if (x <> "") then
-			(* Simulate output of theory loader *)
-			writeln ("Reading " ^ (quote x))
-	               else ()
-	  in
-	     (file_msg thy_file; file_msg ml_file)
-          end
-  in
-    seq loading_msg thys_list
-  end;
-
-
-
-
 (* Temporary hack. *)
 (* 
  NB: this has bad behaviour because update will force loading of
@@ -130,45 +151,43 @@ fun list_loaded_files () =
    this, and to fix it.
 *)
 
-(* 
- Possible alternative: parse "children are out of date"
- message, and unlock those ones (plus descendants).
- This seems feasible, but use_thy ought to do update
- anyway, I think. 
-*)
-
-fun use_thy_and_update thy = 
-  (use_thy_no_topml thy; update(); list_loaded_files());
-
-   
 
 (* configure output channels to decorate output *)
 
 local
+  fun quickout s = TextIO.output (TextIO.stdOut, s);
   fun out s =
     (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
-
-  fun prefix_lines prfx txt =
-    txt |> split_lines |> map (fn s => prfx ^ s ^ "\n") |> implode;
+  fun outnl s =     
+    (TextIO.output (TextIO.stdOut, s^"\n"); TextIO.flushOut TextIO.stdOut);
+
+  fun prefix_lines_specials spec prfx txt sufx =
+    txt |> split_lines |> map (fn s => spec ^ prfx ^ s ^ sufx ^ "\n")
+	|> implode;
+
+  (* Problem with writeln: it's hardwired to do out (s^"\n") but
+     we really want annotations to appear before carriage returns.
+     This hack deals with the last CR in a string.
+  *)	
+  fun out_with_hacked_last_cr startspec str endspec =
+   (quickout startspec;
+    case (rev (split_lines str)) of
+         [] => out endspec
+       | ""::rest => (seq outnl (rev rest);
+		      out endspec)
+       | _ => (quickout str; out endspec))
 in
     (* \240 is octal 360, first special character used. *)
     val _ =
       (prs_fn := 
-	   (fn s => out ("\240" ^ s ^ "\241"));
+	   (fn s => out_with_hacked_last_cr "\240" s "\241");
        warning_fn :=
-	   (fn s => out ("\242" ^ (prefix_lines "### " s) ^ "\243"));
+	   (fn s => out (prefix_lines_specials "\242" "### " s "\243"));
        error_fn :=
-	   (fn s => out ("\244" ^ (prefix_lines "*** " s) ^ "\245")))
+	   (fn s => out (prefix_lines_specials "\244" "*** " s "\245")))
+	   
 end;
 
-(* add specials to ml prompts *)
-
-(* disabled because of bugs *)
-
-(* ml_prompts ">\250" "-\251"; *) (* ?\372, ?\373 *)
-
-
-
 (* add markup to proof state output *)
 
 val proof_state_special_prefix="\246";  (* ?\366 *)
@@ -185,137 +204,38 @@ local
 in
   fun print_current_goals_with_plain_output i j t =
     Library.setmp prs_fn out (print_current_goals_default i j) t;
+
+  (* Annoyingly, Proof General waits for the first prompt before doing
+     anything.  Hack sending a prompt to get things going *)
+
+  val _ = out "> \n";
 end;
 
 print_current_goals_fn := print_current_goals_with_plain_output;
 
 
-(* Turn on verbose update output, Proof General likes to parse it.
-      update_verbose:=true;
-   Unfortunately broken.  We use list_loaded_files instead. *)
-
-(* Get Proof General to cache the loaded files. *)
+(* add specials to ml prompts *)
 
-(* 
-list_loaded_files(); 
-writeln ("Reading "  ^ (quote "wiggle"));
-warning "Could not find blah";
+(*
+   ml_prompts ">\250" "-\251"; (* ?\372, ?\373 *)
+   
+   NB: Obscure bug with proof-shell-annotated-prompt-regexp set
+   properly to include annotations: PG doesn't recognize first proof
+   state output.
+*)   
 
-*)
 
-list_loaded_files();
+(* Turn on verbose update output, Proof General likes to parse it.
+      update_verbose:=true;
+   Unfortunately broken.  We use list_loaded_files instead. *)
 
-(*
-prs "Reading \"/usr/lib/Isabelle98-1/src/HOL/Arith.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Arith.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Integ/Bin.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Integ/Bin.ML\"\n###Could not find file \"CPure.thy\" or \"CPure.ML\" for theory \"CPure\"\n###in the following directories: \".\"\n###File \"CPure.thy\"\n###containing theory \"CPure\" no longer exists.\n###Could not find file \"CPure.thy\" or \"CPure.ML\" for theory \"CPure\"\n###in the following directories: \".\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Datatype.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Divides.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Divides.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Integ/Equiv.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Integ/Equiv.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Finite.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Finite.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Fun.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Fun.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Gfp.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Gfp.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/HOL.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/HOL.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Inductive.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Integ/Int.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Integ/Int.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Integ/IntDef.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Integ/IntDef.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Lfp.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Lfp.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/List.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/List.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Main.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Map.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Map.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Nat.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Nat.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/NatDef.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/NatDef.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Option.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Option.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Ord.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Ord.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Power.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Power.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Prod.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Prod.ML\"\n###Could not find file \"ProtoPure.thy\" or \"ProtoPure.ML\" for theory \"ProtoPure\"\n###in the following directories: \".\"\n###File \"ProtoPure.thy\"\n###containing theory \"ProtoPure\" no longer exists.\n###Could not find file \"ProtoPure.thy\" or \"ProtoPure.ML\" for theory \"ProtoPure\"\n###in the following directories: \".\"\n###Could not find file \"Pure.thy\" or \"Pure.ML\" for theory \"Pure\"\n###in the following directories: \".\"\n###File \"Pure.thy\"\n###containing theory \"Pure\" no longer exists.\n###Could not find file \"Pure.thy\" or \"Pure.ML\" for theory \"Pure\"\n###in the following directories: \".\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Recdef.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Record.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/RelPow.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/RelPow.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Relation.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Relation.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Set.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Set.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Sexp.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Sexp.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/String.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Sum.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Sum.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Trancl.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Trancl.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Univ.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Univ.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Vimage.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/Vimage.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/WF.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/WF.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/WF_Rel.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/WF_Rel.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/equalities.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/equalities.ML\"\nReading \"/home/da/example.thy\"\nReading \"/home/da/example.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/mono.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/mono.ML\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/subset.thy\"\nReading \"/usr/lib/Isabelle98-1/src/HOL/subset.ML\"\n";
+(* Get Proof General to cache the loaded files.  *)
 
-  *)
+ProofGeneral.list_loaded_files();
+ProofGeneral.clear_response_buffer();
+writeln "Isabelle Proof General: Isabelle process ready!";
 
 
 
-(* Modified theory reader stuff
-
-(*Check if a theory file has changed since its last use.
-  Return a pair of boolean values for .thy and for .ML *)
-fun thy_unchanged thy thy_file ml_file =
-  case get_thyinfo thy of
-      Some {thy_time, ml_time, ...} =>
-       let val tn = is_none thy_time;
-           val mn = is_none ml_time
-       in if not tn andalso not mn then
-            ((file_info thy_file = the thy_time),
-             (file_info ml_file = the ml_time))
-          else if not tn andalso mn then
-            (file_info thy_file = the thy_time, false)
-          else
-            (false, false)
-       end
-    | None => (false, false)
-
-(*Remove a theory from loaded_thys *)
-fun remove_thy tname =
-  loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname)
-
-(*Change thy_time and ml_time for an existent item *)
-fun set_info tname thy_time ml_time =
-  let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
-         Some ({path, children, parents, theory, thy_time = _, ml_time = _}) =>
-            {path = path, children = children, parents = parents,
-                     thy_time = thy_time, ml_time = ml_time, theory = theory}
-        | None => error ("set_info: theory " ^ tname ^ " not found");
-  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
-
-                 (Symtab.dest (!loaded_thys)));
-
-(*Mark theory as changed since last read if it has been completly read *)
-fun mark_outdated tname =
-  let val t = get_thyinfo tname;
-  in if is_none t then ()
-     else
-       let val {thy_time, ml_time, ...} = the t
-       in set_info tname (if is_none thy_time then None else Some "")
-                         (if is_none ml_time then None else Some "")
-       end
-  end;
-
-(*Directory given as parameter to use_thy. This is temporarily added to
-  loadpath while the theory's ancestors are loaded.*)
-val tmp_loadpath = ref [] : string list ref;
-
-
-fun update () =
-  let (*List theories in the order they have to be loaded in.*)
-      fun load_order [] result = result
-        | load_order thys result =
-            let fun next_level [] = []
-                  | next_level (t :: ts) =
-                      let val children = children_of t
-                      in children union (next_level ts) end;
-
-                val descendants = next_level thys;
-            in load_order descendants ((result \\ descendants) @ descendants)
-            end;
-
-      fun reload_changed (t :: ts) =
-            let val abspath = case get_thyinfo t of
-                                  Some ({path, ...}) => path
-                                | None => "";
-
-                val (thy_file, ml_file) = get_thy_filenames abspath t;
-		val _ = if thy_file = "" andalso ml_file = "" then
-			error "Giving up"  else ()
-                val (thy_uptodate, ml_uptodate) =
-                        thy_unchanged t thy_file ml_file;
-             in if thy_uptodate andalso ml_uptodate then
- 		(if !update_verbose then
- 	         (writeln
- 		   ("Not reading \"" ^ thy_file ^
- 		          "\" (unchanged)" ^
- 		    (if ml_file <> ""
- 		      then "\nNot reading \"" ^ ml_file ^
- 			   "\" (unchanged)"
- 	              else "")))
- 	         else ())
- 		else use_thy t;
-               reload_changed ts
-            end
-        | reload_changed [] = ();
-
-     (*Remove all theories that are no descendants of ProtoPure.
-       If there are still children in the deleted theory's list
-       schedule them for reloading *)
-     fun collect_garbage no_garbage =
-       let fun collect ((tname, {children, ...}: thy_info) :: ts) =
-                 if tname mem no_garbage then collect ts
-                 else (writeln ("Theory \"" ^ tname ^
-                       "\" is no longer linked with ProtoPure - removing it.");
-                       remove_thy tname;
-                       seq mark_outdated children)
-             | collect [] = ()
-       in collect (Symtab.dest (!loaded_thys)) end;
-  in tmp_loadpath := [];
-     collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] []));
-     reload_changed (load_order ["Pure", "CPure"] [])
-  end;
 
 
-*)