# HG changeset patch
# User wenzelm
# Date 1207832010 -7200
# Node ID 1f09a22a1027b3902a9fdb24a4e962d7e55a3f5f
# Parent  725a3d9011d120e81137f7236aa118f0e573a50b
export get_names (formerly names);
moved pervasive theory = ThyInfo.get_theory to pure_setup.ML;
removed unused pretty_theory;
use OuterSyntax.load_thy instead of backpatched ThyLoad.load_thy;

diff -r 725a3d9011d1 -r 1f09a22a1027 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Apr 10 14:53:29 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Apr 10 14:53:30 2008 +0200
@@ -8,7 +8,6 @@
 
 signature BASIC_THY_INFO =
 sig
-  val theory: string -> theory
   val touch_thy: string -> unit
   val remove_thy: string -> unit
 end;
@@ -19,7 +18,7 @@
   datatype action = Update | Outdate | Remove
   val str_of_action: action -> string
   val add_hook: (action -> string -> unit) -> unit
-  val names: unit -> string list
+  val get_names: unit -> string list
   val known_thy: string -> bool
   val check_known_thy: string -> bool
   val if_known_thy: (string -> unit) -> string -> unit
@@ -29,7 +28,6 @@
   val is_finished: string -> bool
   val loaded_files: string -> Path.T list
   val get_parents: string -> string list
-  val pretty_theory: theory -> Pretty.T
   val touch_child_thys: string -> unit
   val provide_file: Path.T -> string -> unit
   val load_file: bool -> Path.T -> unit
@@ -169,25 +167,6 @@
     error (loader_msg "nothing known about theory" [name]);
 
 
-(* pretty_theory *)
-
-local
-
-fun relevant_names names =
-  let
-    val (finished, unfinished) =
-      List.filter (fn name => name = Context.draftN orelse known_thy name) names
-      |> List.partition (fn name => name <> Context.draftN andalso is_finished name);
-  in (if not (null finished) then [List.last finished] else []) @ unfinished end;
-
-in
-
-fun pretty_theory thy =
-  Pretty.str_list "{" "}" (relevant_names (Context.names_of thy));
-
-end;
-
-
 (* access theory *)
 
 fun lookup_theory name =
@@ -206,7 +185,7 @@
 
 val _ = ML_Context.value_antiq "theory"
   (Scan.lift Args.name
-    >> (fn name => (name ^ "_thy", "ThyInfo.theory " ^ ML_Syntax.print_string name))
+    >> (fn name => (name ^ "_thy", "ThyInfo.get_theory " ^ ML_Syntax.print_string name))
   || Scan.succeed ("thy", "ML_Context.the_global_context ()"));
 
 val _ = ML_Context.value_antiq "theory_ref"
@@ -334,7 +313,7 @@
     val _ = CRITICAL (fn () =>
       change_deps name (Option.map (fn {master, text, parents, files, ...} =>
         make_deps upd_time master text parents files)));
-    val _ = ThyLoad.load_thy dir name pos text (time orelse ! Output.timing);
+    val _ = OuterSyntax.load_thy dir name pos text (time orelse ! Output.timing);
   in
     CRITICAL (fn () =>
      (change_deps name
@@ -609,11 +588,6 @@
 
 fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
 
-
-(*final declarations of this structure*)
-val theory = get_theory;
-val names = get_names;
-
 end;
 
 structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;