src/Pure/Thy/thy_info.ML
changeset 66711 80fa1401cf76
parent 66377 753eb5b83370
child 66873 9953ae603a23
     1.1 --- a/src/Pure/Thy/thy_info.ML	Thu Sep 28 09:42:28 2017 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Sep 28 11:53:55 2017 +0200
     1.3 @@ -160,7 +160,7 @@
     1.4    in res :: map Exn.Exn exns end;
     1.5  
     1.6  datatype task =
     1.7 -  Task of Path.T * string list * (theory list -> result) |
     1.8 +  Task of string list * (theory list -> result) |
     1.9    Finished of theory;
    1.10  
    1.11  fun task_finished (Task _) = false
    1.12 @@ -171,7 +171,7 @@
    1.13  val schedule_seq =
    1.14    String_Graph.schedule (fn deps => fn (_, task) =>
    1.15      (case task of
    1.16 -      Task (_, parents, body) =>
    1.17 +      Task (parents, body) =>
    1.18          let
    1.19            val result = body (task_parents deps parents);
    1.20            val _ = Par_Exn.release_all (join_theory result);
    1.21 @@ -185,7 +185,7 @@
    1.22      val futures = tasks
    1.23        |> String_Graph.schedule (fn deps => fn (name, task) =>
    1.24          (case task of
    1.25 -          Task (_, parents, body) =>
    1.26 +          Task (parents, body) =>
    1.27              (singleton o Future.forks)
    1.28                {name = "theory:" ^ name, group = NONE,
    1.29                  deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
    1.30 @@ -335,19 +335,10 @@
    1.31        |>> forall I
    1.32  and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
    1.33    let
    1.34 -    val {node_name, master_dir, theory_name} = Resources.import_name qualifier dir s;
    1.35 -    fun check_entry (Task (node_name', _, _)) =
    1.36 -          if op = (apply2 File.platform_path (node_name, node_name'))
    1.37 -          then ()
    1.38 -          else
    1.39 -            error ("Incoherent imports for theory " ^ quote theory_name ^
    1.40 -              Position.here require_pos ^ ":\n" ^
    1.41 -              "  " ^ Path.print node_name ^ "\n" ^
    1.42 -              "  " ^ Path.print node_name')
    1.43 -      | check_entry _ = ();
    1.44 +    val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
    1.45    in
    1.46      (case try (String_Graph.get_node tasks) theory_name of
    1.47 -      SOME task => (check_entry task; (task_finished task, tasks))
    1.48 +      SOME task => (task_finished task, tasks)
    1.49      | NONE =>
    1.50          let
    1.51            val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
    1.52 @@ -378,7 +369,7 @@
    1.53                      val load =
    1.54                        load_thy document symbols last_timing initiators update_time dep
    1.55                          text (theory_name, theory_pos) keywords;
    1.56 -                  in Task (node_name, parents, load) end);
    1.57 +                  in Task (parents, load) end);
    1.58  
    1.59            val tasks'' = new_entry theory_name parents task tasks';
    1.60          in (all_current, tasks'') end)