src/Pure/Thy/thy_info.ML
changeset 43673 29eb1cd29961
parent 43651 511df47bcadc
child 43712 3c2c912af2ef
equal deleted inserted replaced
43672:e9f26e66692d 43673:29eb1cd29961
     8 signature THY_INFO =
     8 signature THY_INFO =
     9 sig
     9 sig
    10   datatype action = Update | Remove
    10   datatype action = Update | Remove
    11   val add_hook: (action -> string -> unit) -> unit
    11   val add_hook: (action -> string -> unit) -> unit
    12   val get_names: unit -> string list
    12   val get_names: unit -> string list
       
    13   val status: unit -> unit
    13   val lookup_theory: string -> theory option
    14   val lookup_theory: string -> theory option
    14   val get_theory: string -> theory
    15   val get_theory: string -> theory
    15   val is_finished: string -> bool
    16   val is_finished: string -> bool
    16   val master_directory: string -> Path.T
    17   val master_directory: string -> Path.T
    17   val loaded_files: string -> Path.T list
    18   val loaded_files: string -> Path.T list
    85 (* access thy graph *)
    86 (* access thy graph *)
    86 
    87 
    87 fun thy_graph f x = f (get_thys ()) x;
    88 fun thy_graph f x = f (get_thys ()) x;
    88 
    89 
    89 fun get_names () = Graph.topological_order (get_thys ());
    90 fun get_names () = Graph.topological_order (get_thys ());
       
    91 
       
    92 fun status () =
       
    93   List.app (Output.status o Markup.markup_only o Markup.loaded_theory) (get_names ());
    90 
    94 
    91 
    95 
    92 (* access thy *)
    96 (* access thy *)
    93 
    97 
    94 fun lookup_thy name =
    98 fun lookup_thy name =