# HG changeset patch
# User wenzelm
# Date 968004283 -7200
# Node ID dcf5f9886b8faa21681ffff00e5286c7e6ab7ffe
# Parent  095beeef58aeed32fe3c1ed307dc457a8523059f
added pretend_use_thy_only;

diff -r 095beeef58ae -r dcf5f9886b8f src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Sep 03 20:03:53 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Sep 03 20:04:43 2000 +0200
@@ -41,6 +41,7 @@
   val load_file: bool -> Path.T -> unit
   val use: string -> unit
   val quiet_update_thy: bool -> string -> unit
+  val pretend_use_thy_only: string -> unit
   val begin_theory: (string -> string list -> (Path.T * bool) list -> theory -> theory) ->
     bool -> string -> string list -> (Path.T * bool) list -> theory
   val end_theory: theory -> theory
@@ -265,12 +266,16 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy ml time initiators dir name parents =
+fun load_thy really ml time initiators dir name parents =
   let
-    val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
+    val _ =
+      if really then priority ("Loading theory " ^ quote name ^ required_by " " initiators)
+      else priority ("Registering theory " ^ quote name);
 
     val _ = touch_thy name;
-    val master = ThyLoad.load_thy dir name ml time;
+    val master =
+      if really then ThyLoad.load_thy dir name ml time
+      else #1 (ThyLoad.deps_thy dir name ml);
 
     val files = get_files name;
     val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files;
@@ -310,7 +315,7 @@
               end)
       end);
 
-fun require_thy ml time strict keep_strict initiators prfx (visited, str) =
+fun require_thy really ml time strict keep_strict initiators prfx (visited, str) =
   let
     val path = Path.expand (Path.unpack str);
     val name = Path.pack (Path.base path);
@@ -321,21 +326,22 @@
     else
       let
         val dir = Path.append prfx (Path.dir path);
-        val req_parent =
-          require_thy true time (strict andalso keep_strict) keep_strict (name :: initiators) dir;
+        val req_parent = require_thy true true time (strict andalso keep_strict) keep_strict
+          (name :: initiators) dir;
 
         val (current, (new_deps, parents)) = current_deps ml strict dir name handle ERROR =>
           error (loader_msg "the error(s) above occurred while examining theory" [name] ^
             (if null initiators then "" else required_by "\n" initiators));
         val (visited', parent_results) = foldl_map req_parent (name :: visited, parents);
 
+        val thy = if not really then Some (get_theory name) else None;
         val result =
           if current andalso forall #1 parent_results then true
           else
             ((case new_deps of
-              Some deps => change_thys (update_node name parents (deps, None))
+              Some deps => change_thys (update_node name parents (deps, thy))
             | None => ());
-             load_thy ml (time orelse ! Library.timing) initiators dir name parents;
+             load_thy really ml (time orelse ! Library.timing) initiators dir name parents;
              false);
       in (visited', (result, name)) end
   end;
@@ -348,14 +354,15 @@
 
 in
 
-val weak_use_thy        = gen_use_thy (require_thy true false false false);
-fun quiet_update_thy ml = gen_use_thy (require_thy ml false true true);
+val weak_use_thy        = gen_use_thy (require_thy true true false false false);
+fun quiet_update_thy ml = gen_use_thy (require_thy true ml false true true);
 
-val use_thy          = warn_finished (gen_use_thy (require_thy true false true false));
-val time_use_thy     = warn_finished (gen_use_thy (require_thy true true true false));
-val use_thy_only     = warn_finished (gen_use_thy (require_thy false false true false));
-val update_thy       = warn_finished (gen_use_thy (require_thy true false true true));
-val update_thy_only  = warn_finished (gen_use_thy (require_thy false false true true));
+val use_thy          = warn_finished (gen_use_thy (require_thy true true false true false));
+val time_use_thy     = warn_finished (gen_use_thy (require_thy true true true true false));
+val use_thy_only     = warn_finished (gen_use_thy (require_thy true false false true false));
+val update_thy       = warn_finished (gen_use_thy (require_thy true true false true true));
+val update_thy_only  = warn_finished (gen_use_thy (require_thy true false false true true));
+val pretend_use_thy_only = warn_finished (gen_use_thy (require_thy false false false true false));
 
 end;