# HG changeset patch
# User wenzelm
# Date 1216050704 -7200
# Node ID 7c7a9a343ca5d12f0e6d05addc89739f99a5e707
# Parent  7afff36043e662120062d38ad484b6fc17f1fc14
proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML);
removed obsolete Toplevel.RESTART;

diff -r 7afff36043e6 -r 7c7a9a343ca5 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Jul 14 17:51:43 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Jul 14 17:51:44 2008 +0200
@@ -130,32 +130,25 @@
 
 (* get informed about files *)
 
-local
-
 (*liberal low-level version*)
 val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
-val thy_path = ThyLoad.thy_path o thy_name;
-
-in
-
-fun check_thy "" = false
-  | check_thy file = ThyInfo.check_known_thy (thy_name file);
-
-fun proper_inform_file_processed file () =
-  let
-    val name = thy_name file;
-    val _ = ThyInfo.touch_child_thys name;
-    val _ = ThyInfo.register_thy name handle ERROR msg =>
-      (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
-        tell_file_retracted (thy_path file));
-    val _ = Isar.init_point ();
-  in () end;
-
-fun vacuous_inform_file_processed file () = tell_file_retracted (thy_path file);
 
 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
 
-end;
+fun inform_file_processed file =
+  let
+    val name = thy_name file;
+    val _ = name = "" andalso error ("Bad file name: " ^ quote file);
+    val _ =
+      if ThyInfo.check_known_thy name then
+        (Isar.commit_exit ();
+          ThyInfo.touch_child_thys name;
+          ThyInfo.register_thy name handle ERROR msg =>
+            (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
+             tell_file_retracted (ThyLoad.thy_path name)))
+      else ();
+    val _ = Isar.init_point ();
+  in () end;
 
 
 (* restart top-level loop (keeps most state information) *)
@@ -167,8 +160,7 @@
   tell_clear_goals ();
   tell_clear_response ();
   Isar.init_point ();
-  welcome ();
-  raise Toplevel.RESTART);
+  welcome ());
 
 
 (* theorem dependency output *)
@@ -219,11 +211,8 @@
 
 fun inform_file_processedP () =
   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
-    (P.name >> (fn file => Toplevel.no_timing o
-      Toplevel.imperative (fn () => error "Bad file name") o
-      Toplevel.init_empty (fn _ => file <> "") (vacuous_inform_file_processed file) o
-      Toplevel.kill o
-      Toplevel.init_empty (fn _ => check_thy file) (proper_inform_file_processed file)));
+    (P.name >> (fn file =>
+      Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
 
 fun inform_file_retractedP () =
   OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control