src/Pure/Thy/thy_info.ML

 
 (* load_file *)
 
 local
 
-fun provide path name info (deps as SOME {update_time, master, text, parents, files}) =
+fun provide path name info (SOME {update_time, master, text, parents, files}) =
      (if AList.defined (op =) files path then ()
       else warning (loader_msg "undeclared dependency of theory" [name] ^
         " on file: " ^ quote (Path.implode path));
       SOME (make_deps update_time master text parents
         (AList.update (op =) (path, SOME info) files)))

   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
 fun load_thy time upd_time initiators name =
   let
     val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
-    val (pos, text, files) =
+    val (pos, text, _) =
       (case get_deps name of
         SOME {master = SOME (master_path, _), text as _ :: _, files, ...} =>
           (Path.position master_path, text, files)
       | _ => error (loader_msg "corrupted dependency information" [name]));
     val _ = touch_thy name;

         in after_load () handle exn => (kill_thy name; reraise exn) end
     | _ => ()));
 
 in
 
-fun schedule_tasks tasks n =
+fun schedule_tasks tasks =
   if not (Multithreading.enabled ()) then schedule_seq tasks
   else if Multithreading.self_critical () then
      (warning (loader_msg "no multithreading within critical section" []);
       schedule_seq tasks)
   else schedule_futures tasks;

   (case lookup_deps name of
     SOME NONE => (true, NONE, get_parents name)
   | NONE =>
       let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name
       in (false, init_deps (SOME master) text parents files, parents) end
-  | SOME (deps as SOME {update_time, master, text, parents, files}) =>
+  | SOME (SOME {update_time, master, text, parents, files}) =>
       let
         val (thy_path, thy_id) = ThyLoad.check_thy dir name;
         val master' = SOME (thy_path, thy_id);
       in
         if Option.map #2 master <> SOME thy_id then

     val path = Path.expand (Path.explode str);
     val name = Path.implode (Path.base path);
     val dir' = Path.append dir (Path.dir path);
     val _ = member (op =) initiators name andalso error (cycle_msg initiators);
   in
-    (case try (Graph.get_node (fst tasks)) name of
+    (case try (Graph.get_node tasks) name of
       SOME task => (task_finished task, tasks)
     | NONE =>
         let
           val (current, deps, parents) = check_deps dir' name
             handle ERROR msg => cat_error msg
               (loader_msg "the error(s) above occurred while examining theory" [name] ^
                 required_by "\n" initiators);
           val parent_names = map base_name parents;
 
-          val (parents_current, (tasks_graph', tasks_len')) =
+          val (parents_current, tasks_graph') =
             require_thys time (name :: initiators)
               (Path.append dir (master_dir' deps)) parents tasks;
 
           val all_current = current andalso parents_current;
           val _ = if not all_current andalso known_thy name then outdate_thy name else ();

 
           val upd_time = serial ();
           val tasks_graph'' = tasks_graph' |> new_deps name parent_names
            (if all_current then Finished
             else Task (fn () => load_thy time upd_time initiators name));
-          val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1;
-        in (all_current, (tasks_graph'', tasks_len'')) end)
+        in (all_current, tasks_graph'') end)
   end;
 
 end;
 
 
 (* use_thy etc. *)
 
 local
 
 fun gen_use_thy' req dir arg =
-  let val (_, (tasks, n)) = req [] dir arg (Graph.empty, 0)
-  in schedule_tasks tasks n end;
+  schedule_tasks (snd (req [] dir arg Graph.empty));
 
 fun gen_use_thy req str =
   let val name = base_name str in
     check_unfinished warning name;
     gen_use_thy' req Path.current str