src/Pure/PIDE/document.ML
changeset 65445 e9e7f5f5794c
parent 65357 9a2c266f97c8
child 66167 1bd268ab885c
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Apr 08 21:35:04 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Apr 08 22:36:32 2017 +0200
     1.3 @@ -177,9 +177,6 @@
     1.4      SOME eval => Command.eval_finished eval
     1.5    | NONE => false);
     1.6  
     1.7 -fun loaded_theory name =
     1.8 -  get_first Thy_Info.lookup_theory [name, Long_Name.base_name name];
     1.9 -
    1.10  fun get_node nodes name = String_Graph.get_node nodes name
    1.11    handle String_Graph.UNDEF _ => empty_node;
    1.12  fun default_node name = String_Graph.default_node (name, empty_node);
    1.13 @@ -463,7 +460,7 @@
    1.14        val delay_request' = Event_Timer.future (Time.now () + delay);
    1.15  
    1.16        fun finished_import (name, (node, _)) =
    1.17 -        finished_result node orelse is_some (loaded_theory name);
    1.18 +        finished_result node orelse is_some (Thy_Info.lookup_theory name);
    1.19  
    1.20        val nodes = nodes_of (the_version state version_id);
    1.21        val required = make_required nodes;
    1.22 @@ -530,7 +527,7 @@
    1.23          handle ERROR msg => (Output.error_message msg; NONE);
    1.24      val parents_reports =
    1.25        imports |> map_filter (fn (import, pos) =>
    1.26 -        (case loaded_theory import of
    1.27 +        (case Thy_Info.lookup_theory import of
    1.28            NONE =>
    1.29              maybe_end_theory pos
    1.30                (case get_result (snd (the (AList.lookup (op =) deps import))) of
    1.31 @@ -554,7 +551,7 @@
    1.32    else NONE;
    1.33  
    1.34  fun check_theory full name node =
    1.35 -  is_some (loaded_theory name) orelse
    1.36 +  is_some (Thy_Info.lookup_theory name) orelse
    1.37    null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
    1.38  
    1.39  fun last_common keywords state node_required node0 node =