fork diagnostic commands (theory loader and PIDE interaction);
authorwenzelm
Tue Feb 26 19:44:26 2013 +0100 (2013-02-26 ago)
changeset 5128459a03019f3bf
parent 51283 fefd07697979
child 51285 0859bd338c9b
fork diagnostic commands (theory loader and PIDE interaction);
explicit id for load_thy, for more robust Goal.fork accounting and commit for each theory -- NB: use_thys nodes become subject to Position.is_reported like PIDE document transactions;
clarified Toplevel.command_exception vs. Toplevel.command_errors;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Feb 26 13:38:34 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Feb 26 19:44:26 2013 +0100
     1.3 @@ -94,8 +94,9 @@
     1.4    val get_timing: transition -> Time.time
     1.5    val put_timing: Time.time -> transition -> transition
     1.6    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     1.7 -  val command: transition -> state -> state
     1.8 -  val atom_result: transition -> state -> (transition * state) * state
     1.9 +  val command_exception: bool -> transition -> state -> state
    1.10 +  val command_errors: bool -> transition -> state ->
    1.11 +    ((serial * string) * string option) list * state option
    1.12    val element_result: transition Thy_Syntax.element -> state ->
    1.13      (transition * state) list future * state
    1.14  end;
    1.15 @@ -685,15 +686,21 @@
    1.16  end;
    1.17  
    1.18  
    1.19 -(* nested commands *)
    1.20 +(* managed commands *)
    1.21  
    1.22 -fun command tr st =
    1.23 -  (case transition (! interact) tr st of
    1.24 +fun command_exception int tr st =
    1.25 +  (case transition int tr st of
    1.26      SOME (st', NONE) => st'
    1.27    | SOME (_, SOME (exn, info)) =>
    1.28        if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
    1.29    | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
    1.30  
    1.31 +fun command_errors int tr st =
    1.32 +  (case transition int tr st of
    1.33 +    SOME (st', NONE) => ([], SOME st')
    1.34 +  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
    1.35 +  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
    1.36 +
    1.37  
    1.38  (* scheduled proof result *)
    1.39  
    1.40 @@ -710,12 +717,19 @@
    1.41      else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1)
    1.42    end;
    1.43  
    1.44 -fun atom_result tr st =
    1.45 -  let val st' = command tr st
    1.46 -  in ((tr, st'), st') end;
    1.47 -
    1.48  fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
    1.49    let
    1.50 +    val command = command_exception (! interact);
    1.51 +
    1.52 +    fun atom_result tr st =
    1.53 +      let
    1.54 +        val st' =
    1.55 +          if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
    1.56 +            setmp_thread_position tr (fn () =>
    1.57 +              (Goal.fork_name "Toplevel.diag" (priority [tr]) (fn () => command tr st); st)) ()
    1.58 +          else command tr st;
    1.59 +      in ((tr, st'), st') end;
    1.60 +
    1.61      val proof_trs =
    1.62        (case opt_proof of
    1.63          NONE => []
    1.64 @@ -735,13 +749,14 @@
    1.65  
    1.66          val future_proof = Proof.global_future_proof
    1.67            (fn prf =>
    1.68 -            Goal.fork_name "Toplevel.future_proof" (priority proof_trs)
    1.69 -              (fn () =>
    1.70 -                let val (result, result_state) =
    1.71 -                  (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.72 -                    => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.73 -                  |> fold_map atom_result body_trs ||> command end_tr;
    1.74 -                in (result, presentation_context_of result_state) end))
    1.75 +            setmp_thread_position head_tr (fn () =>
    1.76 +              Goal.fork_name "Toplevel.future_proof" (priority proof_trs)
    1.77 +                (fn () =>
    1.78 +                  let val (result, result_state) =
    1.79 +                    (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.80 +                      => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.81 +                    |> fold_map atom_result body_trs ||> command end_tr;
    1.82 +                  in (result, presentation_context_of result_state) end)) ())
    1.83            #-> Result.put;
    1.84  
    1.85          val st'' = st'
     2.1 --- a/src/Pure/PIDE/command.ML	Tue Feb 26 13:38:34 2013 +0100
     2.2 +++ b/src/Pure/PIDE/command.ML	Tue Feb 26 19:44:26 2013 +0100
     2.3 @@ -62,10 +62,11 @@
     2.4  local
     2.5  
     2.6  fun run int tr st =
     2.7 -  (case Toplevel.transition int tr st of
     2.8 -    SOME (st', NONE) => ([], SOME st')
     2.9 -  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
    2.10 -  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
    2.11 +  if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
    2.12 +    Toplevel.setmp_thread_position tr (fn () =>
    2.13 +      (Goal.fork_name "Toplevel.diag" ~1
    2.14 +        (fn () => Toplevel.command_exception int tr st); ([], SOME st))) ()
    2.15 +  else Toplevel.command_errors int tr st;
    2.16  
    2.17  fun check_cmts tr cmts st =
    2.18    Toplevel.setmp_thread_position tr
     3.1 --- a/src/Pure/Thy/thy_info.ML	Tue Feb 26 13:38:34 2013 +0100
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Feb 26 19:44:26 2013 +0100
     3.3 @@ -164,7 +164,7 @@
     3.4  
     3.5  (* scheduling loader tasks *)
     3.6  
     3.7 -type result = theory * unit future * (unit -> unit);
     3.8 +type result = theory * serial * unit future * (unit -> unit);
     3.9  
    3.10  datatype task =
    3.11    Task of string list * (theory list -> result) |
    3.12 @@ -177,8 +177,14 @@
    3.13  
    3.14  local
    3.15  
    3.16 -fun finish_thy ((thy, present, commit): result) =
    3.17 -  (Thm.join_theory_proofs thy; Future.join present; commit (); thy);
    3.18 +fun finish_thy ((thy, id, present, commit): result) =
    3.19 +  let
    3.20 +    val result1 = Exn.capture Thm.join_theory_proofs thy;
    3.21 +    val results2 = Future.join_results (Goal.peek_futures id);
    3.22 +    val result3 = Future.join_result present;
    3.23 +    val _ = Par_Exn.release_all (result1 :: results2 @ [result3]);
    3.24 +    val _ = commit ();
    3.25 +  in thy end;
    3.26  
    3.27  val schedule_seq =
    3.28    String_Graph.schedule (fn deps => fn (_, task) =>
    3.29 @@ -186,22 +192,29 @@
    3.30        Task (parents, body) => finish_thy (body (task_parents deps parents))
    3.31      | Finished thy => thy)) #> ignore;
    3.32  
    3.33 -val schedule_futures = uninterruptible (fn _ =>
    3.34 -  String_Graph.schedule (fn deps => fn (name, task) =>
    3.35 -    (case task of
    3.36 -      Task (parents, body) =>
    3.37 -        (singleton o Future.forks)
    3.38 -          {name = "theory:" ^ name, group = NONE,
    3.39 -            deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
    3.40 -          (fn () =>
    3.41 -            (case filter (not o can Future.join o #2) deps of
    3.42 -              [] => body (map (#1 o Future.join) (task_parents deps parents))
    3.43 -            | bad =>
    3.44 -                error (loader_msg ("failed to load " ^ quote name ^
    3.45 -                  " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
    3.46 -    | Finished thy => Future.value (thy, Future.value (), I)))
    3.47 -  #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn])
    3.48 -  #> rev #> Par_Exn.release_all) #> ignore;
    3.49 +val schedule_futures = uninterruptible (fn _ => fn tasks =>
    3.50 +  let
    3.51 +    val results1 = tasks
    3.52 +      |> String_Graph.schedule (fn deps => fn (name, task) =>
    3.53 +        (case task of
    3.54 +          Task (parents, body) =>
    3.55 +            (singleton o Future.forks)
    3.56 +              {name = "theory:" ^ name, group = NONE,
    3.57 +                deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
    3.58 +              (fn () =>
    3.59 +                (case filter (not o can Future.join o #2) deps of
    3.60 +                  [] => body (map (#1 o Future.join) (task_parents deps parents))
    3.61 +                | bad =>
    3.62 +                    error (loader_msg ("failed to load " ^ quote name ^
    3.63 +                      " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
    3.64 +        | Finished thy => Future.value (thy, 0, Future.value (), I)))
    3.65 +      |> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn]);
    3.66 +
    3.67 +    (* FIXME avoid global reset_futures (!??) *)
    3.68 +    val results2 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ()));
    3.69 +
    3.70 +    val _ = Par_Exn.release_all (rev (results2 @ results1));
    3.71 +  in () end);
    3.72  
    3.73  in
    3.74  
    3.75 @@ -234,11 +247,13 @@
    3.76  
    3.77      val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
    3.78  
    3.79 +    val id = serial ();
    3.80 +    val text_pos = Position.put_id (Markup.print_int id) (Path.position thy_path);
    3.81      val (theory, present) =
    3.82 -      Thy_Load.load_thy last_timing update_time dir header (Path.position thy_path) text
    3.83 +      Thy_Load.load_thy last_timing update_time dir header text_pos text
    3.84          (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
    3.85      fun commit () = update_thy deps theory;
    3.86 -  in (theory, present, commit) end;
    3.87 +  in (theory, id, present, commit) end;
    3.88  
    3.89  fun check_deps dir name =
    3.90    (case lookup_deps name of