src/Pure/Thy/thy_info.ML
changeset 7935 ac62465ed06c
parent 7910 e54db490c537
child 7941 653964583bd3
equal deleted inserted replaced
7934:42836b6c4c73 7935:ac62465ed06c
    27   datatype action = Update | Outdate | Remove
    27   datatype action = Update | Outdate | Remove
    28   val str_of_action: action -> string
    28   val str_of_action: action -> string
    29   val add_hook: (action -> string -> unit) -> unit
    29   val add_hook: (action -> string -> unit) -> unit
    30   val names: unit -> string list
    30   val names: unit -> string list
    31   val known_thy: string -> bool
    31   val known_thy: string -> bool
       
    32   val check_known_thy: string -> bool
       
    33   val if_known_thy: (string -> unit) -> string -> unit
    32   val lookup_theory: string -> theory option
    34   val lookup_theory: string -> theory option
    33   val get_theory: string -> theory
    35   val get_theory: string -> theory
    34   val get_preds: string -> string list
    36   val get_preds: string -> string list
    35   val loaded_files: string -> Path.T option * (Path.T * bool) list
    37   val loaded_files: string -> Path.T list
    36   val touch_child_thys: string -> unit
    38   val touch_child_thys: string -> unit
    37   val touch_all_thys: unit -> unit
    39   val touch_all_thys: unit -> unit
    38   val may_load_file: bool -> bool -> Path.T -> unit
    40   val may_load_file: bool -> bool -> Path.T -> unit
    39   val use_path: Path.T -> unit
    41   val use_path: Path.T -> unit
    40   val use: string -> unit
    42   val use: string -> unit
   120 fun get_names () = Graph.keys (get_thys ());
   122 fun get_names () = Graph.keys (get_thys ());
   121 
   123 
   122 
   124 
   123 (* access thy *)
   125 (* access thy *)
   124 
   126 
   125 fun lookup_thy name = Some (thy_graph Graph.get_node name) handle Graph.UNDEFINED _ => None;
   127 fun lookup_thy name =
       
   128   Some (thy_graph Graph.get_node name) handle Graph.UNDEFINED _ => None;
       
   129 
   126 val known_thy = is_some o lookup_thy;
   130 val known_thy = is_some o lookup_thy;
       
   131 fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false);
       
   132 fun if_known_thy f name = if check_known_thy name then f name else ();
   127 
   133 
   128 fun get_thy name =
   134 fun get_thy name =
   129   (case lookup_thy name of
   135   (case lookup_thy name of
   130     Some thy => thy
   136     Some thy => thy
   131   | None => error (loader_msg "nothing known about theory" [name]));
   137   | None => error (loader_msg "nothing known about theory" [name]));
   142 fun is_finished name = is_none (get_deps name);
   148 fun is_finished name = is_none (get_deps name);
   143 fun get_files name = (case get_deps name of Some {files, ...} => files | _ => []);
   149 fun get_files name = (case get_deps name of Some {files, ...} => files | _ => []);
   144 
   150 
   145 fun loaded_files name =
   151 fun loaded_files name =
   146   (case get_deps name of
   152   (case get_deps name of
   147     None => (None, [])
   153     None => []
   148   | Some {master, files, ...} =>
   154   | Some {master, files, ...} =>
   149       (apsome (#1 o ThyLoad.get_thy) master,
   155       (case master of Some m => [#1 (ThyLoad.get_thy m)] | None => []) @
   150         map (fn ((p, _), r) => (p, r)) (mapfilter #2 files)));
   156         map (#1 o #1) (mapfilter #2 files));
   151 
   157 
   152 fun get_preds name =
   158 fun get_preds name =
   153   (thy_graph Graph.imm_preds name) handle Graph.UNDEFINED _ =>
   159   (thy_graph Graph.imm_preds name) handle Graph.UNDEFINED _ =>
   154     error (loader_msg "nothing known about theory" [name]);
   160     error (loader_msg "nothing known about theory" [name]);
   155 
   161