obsolete, use Isabelle's native ProofGeneral.init instead;

1 files changed, 0 insertions, 409 deletions

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
deleted file mode 100644
index 293eac39..00000000
--- a/isa/ProofGeneral.ML
+++ /dev/null
@@ -1,409 +0,0 @@
-(* 
-   Isabelle configuration for Proof General.
-
-   Author:  David Aspinall <da@dcs.ed.ac.uk>
-   Contact: Isabelle maintainer <isabelle@dcs.ed.ac.uk>
-
-   $Id$
-
-*)
-
-signature PROOFGENERAL =
-sig
-   val kill_goal : unit -> unit
-   val help : unit -> unit
-   val show_context : unit -> theory
-   val repeat_undo : int -> unit
-   val clear_response_buffer : unit -> unit
-   val clear_goals_buffer : unit -> unit
-
-   (* Processing used files *)
-   
-   val retract_ML_files_children : string -> unit
-   val retract_thy_file : string -> unit
-   val list_loaded_files : unit -> unit
-   val restart : unit -> unit
-   val use_thy : string -> unit
-   val update : unit -> unit
-   
-   (* not used *)
-   val retract_ML_file : string -> unit
-   val use_thy_and_update : string -> unit
-
-   (*  visible only for testing *)
-   val loaded_parents_of : string -> string list
-   val loaded_files : unit -> string list
-   val apply_and_update_files : ('a -> 'b) -> 'a -> unit
-   val initial_loaded_thys : thy_info Symtab.table ref
-   val special_theories : string list ref
-   val retracted_files : string list ref
-end;
-
-structure ProofGeneral : PROOFGENERAL =
-  struct
-    (* State *)
-
-    (* Theories which have no .thy or .ML files *)	
-    val special_theories = ref ["ProtoPure", "Pure", "CPure"];
-
-    (* Cache of retracted files: see notes below. *)
-    val retracted_files = ref [] : string list ref;
-
-    (* Copy of theory database *)
-    val initial_loaded_thys = ref (!loaded_thys);
-
-    (* Messages to Proof General *)
-
-    fun retract_msg x = writeln ("Proof General, you can unlock the file "
-			         ^ (quote x))
-    fun process_msg x = writeln ("Proof General, this file is loaded: "
-			         ^ (quote x))
-    fun msg_unless_empty f x = if (x<>"") then f x else ();
-
-    fun clear_response_buffer () =
-       writeln("Proof General, please clear the response buffer.");
-
-    fun clear_goals_buffer () =
-       writeln("Proof General, please clear the goals buffer.");
-
-
-    (* Some top-level commands for Proof General. *)
-
-    fun kill_goal () = (Goal "PROP no_goal_supplied"; clear_goals_buffer())
-    fun help () = print version;
-    fun show_context () = the_context();
-
-    (* Function used by undo operation *)
-    
-    fun repeat_undo 0 = ()
-      | repeat_undo n = (undo(); repeat_undo (n-1));
-
-
-       
-
-    (*
-      FIXME future function, to help synchronize in event of an error.
-      fun clear_msg x = writeln
-        ("Proof General, please clear your record of loaded files.")
-    *)
-
-    (*  Functions used internally by Proof General to track
-        dependencies between theory and ML files. *)
-
-   (* LISTING LOADED FILES
-        Next few functions tell Proof General what files are
-	loaded into Isabelle.
-    *)
-      	
-   (* subroutine: return loaded files for theory named tname *)
-   fun loaded_files_for thys =
-     let fun loaded_for tname =
-     if (tname mem (!special_theories)) then [] else
-	let val (path,thy_time,ml_time) =
-	      (case Symtab.lookup (!loaded_thys, tname) of
-	         (Some {path, thy_time, ml_time, ...}) =>
-		 (path, is_some thy_time, is_some ml_time)
-	       | None => ("",false,false))  (* shouldn't happen *)
-	    val (thy_file,ml_file) = get_thy_filenames path tname
-	    fun file_name x = if (x <> "") then [x] else []
-	in
-	  (if thy_time then (file_name thy_file) else [])
-	   @
-	  (if ml_time then (file_name ml_file) else [])
-	 end
-     in
-        foldl (op @) ([], map loaded_for thys)
-     end 
-
-   (* Return a list of the loaded files in the theory database *)
-   fun loaded_files () = loaded_files_for
-				(map fst (Symtab.dest (!loaded_thys)))
-
-   (* List all the loaded files in the theory database.
-      Clears the list of retracted files.
-   *)
-   fun list_loaded_files () =
-   let
-     val _ = retracted_files := []
-   in     
-    (writeln "Setting loaded files list...";
-     seq (msg_unless_empty process_msg) (loaded_files());
-     writeln "Done.")
-   end
-
-   (* RESTARTING *)
-
-   fun restart () =
-     let val _ = (loaded_thys := !initial_loaded_thys)
-         val _ = (retracted_files := [])
-      in
-         (list_loaded_files();
-          clear_response_buffer();
-	  (* The goals output from this command is ignored because
-             its followed by an urgent message. *)
-	  kill_goal();	
-          writeln "Isabelle Proof General: Isabelle process ready!")
-      end;
-
-
-    (*
-      RETRACTION:
-         We keep some state here to record what files Proof General
-	 thinks have been retracted.
-	 Really this shouldn't be necessary but it gets round
-	 some of the mess of the theory loader.
-	 
-     *)
-
-    (* subroutine: retract a file and give message, if it hasn't
-       been already reported to Proof General. *)
-       
-    fun retract_file_and_give_message filename msg_flag =
-      if filename="" orelse (filename mem !retracted_files) then ()
-      else (if msg_flag then (retract_msg filename) else ();
-	    retracted_files := filename :: !retracted_files;
-	    ())
-
-    fun retract_file1 not_thy only_report_children filename =
-     let val (path, tname) = split_filename filename
-         fun show_msgs thy =
-           let val (thy_file, ml_file) = get_thy_filenames (path_of thy) thy
-            in (if not_thy then ()
-		   else retract_file_and_give_message thy_file true; 
-		retract_file_and_give_message ml_file 
-					(not only_report_children)) end
-         (* Considered loaded if either theory or ML times set *)
-	 fun already_loaded thy =
-           let val t = get_thyinfo thy
-           in if is_none t then false
-              else let val {thy_time, ml_time, ...} = the t
-           in is_some thy_time orelse is_some ml_time end
-         end
-
-         fun children_loaded thy = 
-         let val children = children_of thy
-	     val present = filter (is_some o get_thyinfo) children;
-          in filter already_loaded present end
-      in      
-       if already_loaded tname then
-	 (show_msgs tname; 
-	  map (retract_file1 false false) (children_loaded tname); ())
-       else ()
-   end;
-
-   (* retract a script file and all it's theory/script children,
-      but not it's parent theory. *)
-
-   val retract_ML_file = retract_file1 true false;
-
-   (* Same as above, but only give reports to Proof General for
-      the children.  *)
-
-   val retract_ML_files_children = retract_file1 true true;
-
-
-   (* retract a theory file and all it's theory/script children *)
-
-   val retract_thy_file = retract_file1 false false;
-
-
-   (* USING files.
-        When a file is used by Isabelle, Proof General wants to know
-	all it's ancestor files which are loaded automatically.
-	The theory loader only loads files if they've changed,
-	so we use the cache of retracted files to pretend more
-	have been loaded.
-    *)
-
-   (* Find the loaded parents of a file (including the file itself) *)
-   fun loaded_parents_of filename =
-   let
-      val (path, tname) = split_filename filename
-      fun already_loaded thy =
-      let val t = get_thyinfo thy
-       in if is_none t then false
-          else let val {thy_time, ml_time, ...} = the t
-        in is_some thy_time orelse is_some ml_time end
-      end
-      fun gather_parents parents thys =
-	 let val next_parents = foldl (op union) ([],map parents_of_name thys)
-	     val interesting_parents = filter already_loaded next_parents
-	     val new_parents = interesting_parents \\ parents
-	  in case new_parents of
-	       [] => parents
-	     | _ => gather_parents (parents union new_parents) new_parents
-	  end
-      in      
-       if (already_loaded tname) 
-       then loaded_files_for (gather_parents [tname] [tname])
-       else []
-   end;
-
-   (*  List the parents of a loaded file *)
-   (* not used *)   
-   fun list_parents_with f filename =
-      seq (msg_unless_empty f) (loaded_parents_of filename)
-      
-   (* Function to do a "use" operation.
-       Only report the newly loaded parents of a theory, because its
-       children should be unlocked at this point, and not get
-       locked by the use operation.
-
-       The current loaded files are taken to be those really loaded
-       less the ones considered retracted.  Newly loaded parents are
-       the new files loaded which are parents afterwards.
-
-       This all assumes that a use operation only loads parents. 
-       Using a theory can lock new files which are parents of the
-       theory being used. It cannot unlock files.
-    *)
-           
-     fun use_thy1 use_fn thy =
-     let
-      val loaded_before = (loaded_files()) \\ (!retracted_files)
-      val _ = (use_fn thy) handle ex =>
-			(list_loaded_files(); raise ex)
-      val parents_after = loaded_parents_of thy
-      val parents_added = parents_after \\ loaded_before
-      val _ = retracted_files := ((!retracted_files) \\ parents_added)
-     in     
-       (seq process_msg parents_added)
-     end
-
-     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, thy_time = thy_time, ml_time = None }
-             | None => error 
-	 ("remove_mlfile_from_db: theory " ^ thy ^ " not found");
-    in  loaded_thys := Symtab.update ((thy, tinfo), !loaded_thys) end;
-     
-    (* Use a theory file but not it's top-level ML file *)
-    val use_thy =
-      let fun use_fn file =
-          let val _ = use_thy_no_topml file
-              val (_, tname) = split_filename file
-              val _ = remove_mlfile_fromdb tname   (*fix bug in thy_no_topml*)
-          in () end
-       in use_thy1 use_fn end;
-    
-
-   (* Function to do an "update" operation.
-       This is like the use operation above except that we
-       consider all of the loaded files, since update can make
-       change anywhere.   It may also load top-level ML
-       files which is a bit of a nuisance.
-    *)
-
-   fun apply_and_update_files update_fn x =
-   let val files_before = loaded_files() \\ !retracted_files
-       val _ = update_fn x
-       val files_after = loaded_files()
-       val files_added = files_after \\ files_before 
-       val files_removed = files_before \\ files_after
-    in
-      (seq retract_msg files_removed;
-       seq process_msg files_added)
-    end
-
-  (* Update and re-list loaded files and deletions. *)
-  val update = apply_and_update_files update;
-
-
-  (* not used *)
-  fun use_thy_and_update thy = 
-  (use_thy_no_topml thy;
-   update();
-   list_loaded_files();
-   clear_response_buffer())
-
- end; (* struct ProofGeneral *)
-
-
-(* 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 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_with_hacked_last_cr "\240" s "\241");
-       warning_fn :=
-	   (fn s => out (prefix_lines_specials "\242" "### " s "\243"));
-       error_fn :=
-	   (fn s => out (prefix_lines_specials "\244" "*** " s "\245")))
-	   
-end;
-
-(* add markup to proof state output *)
-
-val proof_state_special_prefix="\246";  (* ?\366 *)
-val proof_state_special_suffix="\247";  (* ?\367 *)
-val goal_start_special="\248";	        (* ?\370 *)
-
-current_goals_markers:=(proof_state_special_prefix,
-			proof_state_special_suffix,
-		        goal_start_special);
-
-local
-  fun out s =
-    (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
-in
-  fun print_current_goals_with_plain_output i j t =
-    Library.setmp prs_fn out (print_current_goals_default i j) t;
-
-(* Proof General has problems sending commands outside of the
-   action list.  Also, it waits for the first prompt before doing
-   anything.  The next function hacks sending a prompt to get
-   things going and to help fix things later. *)
-
-  fun hack_send_prompt _ = out ">\250 \n";
-end;
-
-print_current_goals_fn := print_current_goals_with_plain_output;
-
-
-(* add specials to ml prompts *)
-
-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.
-*)   
-
-
-(* Turn on verbose update output, Proof General likes to parse it.
-      update_verbose:=true;
-   Unfortunately broken.  We use list_loaded_files instead. *)
-
-
-(* Wake up, Proof General! *)
-(* hack_send_prompt(); *)
-
-(* Get Proof General to cache the loaded files.  *)
-ProofGeneral.restart();