tuned signature;
authorwenzelm
Wed Apr 06 17:16:30 2016 +0200 (2016-04-06 ago)
changeset 628917a11ea5c9626
parent 62890 728aa05e9433
child 62892 7485507620b6
tuned signature;
src/Pure/Concurrent/event_timer.ML
src/Pure/Concurrent/lazy.ML
src/Pure/Concurrent/multithreading.ML
src/Pure/Concurrent/par_list.ML
src/Pure/Concurrent/single_assignment.ML
src/Pure/Concurrent/synchronized.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/Concurrent/thread_data.ML
src/Pure/Concurrent/unsynchronized.ML
src/Pure/ML/exn_debugger.ML
src/Pure/ML/exn_properties.ML
src/Pure/PIDE/execution.ML
src/Pure/PIDE/query_operation.ML
src/Pure/System/bash.ML
src/Pure/System/command_line.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/windows/bash.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/debugger.ML
     1.1 --- a/src/Pure/Concurrent/event_timer.ML	Wed Apr 06 16:51:52 2016 +0200
     1.2 +++ b/src/Pure/Concurrent/event_timer.ML	Wed Apr 06 17:16:30 2016 +0200
     1.3 @@ -109,7 +109,7 @@
     1.4        manager_loop);
     1.5  
     1.6  fun shutdown () =
     1.7 -  uninterruptible (fn restore_attributes => fn () =>
     1.8 +  Multithreading.uninterruptible (fn restore_attributes => fn () =>
     1.9      if Synchronized.change_result state (fn st as State {requests, manager, ...} =>
    1.10        if is_shutdown Normal st then (false, st)
    1.11        else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then
    1.12 @@ -144,7 +144,7 @@
    1.13        val manager' = manager_check manager;
    1.14      in (canceled, make_state (requests', status, manager')) end);
    1.15  
    1.16 -val future = uninterruptible (fn _ => fn time =>
    1.17 +val future = Multithreading.uninterruptible (fn _ => fn time =>
    1.18    let
    1.19      val req: request Single_Assignment.var = Single_Assignment.var "request";
    1.20      fun abort () = ignore (cancel (Single_Assignment.await req));
     2.1 --- a/src/Pure/Concurrent/lazy.ML	Wed Apr 06 16:51:52 2016 +0200
     2.2 +++ b/src/Pure/Concurrent/lazy.ML	Wed Apr 06 17:16:30 2016 +0200
     2.3 @@ -61,7 +61,7 @@
     2.4    (case peek (Lazy var) of
     2.5      SOME res => res
     2.6    | NONE =>
     2.7 -      uninterruptible (fn restore_attributes => fn () =>
     2.8 +      Multithreading.uninterruptible (fn restore_attributes => fn () =>
     2.9          let
    2.10            val (expr, x) =
    2.11              Synchronized.change_result var
     3.1 --- a/src/Pure/Concurrent/multithreading.ML	Wed Apr 06 16:51:52 2016 +0200
     3.2 +++ b/src/Pure/Concurrent/multithreading.ML	Wed Apr 06 17:16:30 2016 +0200
     3.3 @@ -4,21 +4,16 @@
     3.4  Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
     3.5  *)
     3.6  
     3.7 -signature BASIC_MULTITHREADING =
     3.8 -sig
     3.9 -  val interruptible: ('a -> 'b) -> 'a -> 'b
    3.10 -  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
    3.11 -end;
    3.12 -
    3.13  signature MULTITHREADING =
    3.14  sig
    3.15 -  include BASIC_MULTITHREADING
    3.16    val no_interrupts: Thread.threadAttribute list
    3.17    val public_interrupts: Thread.threadAttribute list
    3.18    val private_interrupts: Thread.threadAttribute list
    3.19    val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
    3.20    val interrupted: unit -> unit  (*exception Interrupt*)
    3.21    val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
    3.22 +  val interruptible: ('a -> 'b) -> 'a -> 'b
    3.23 +  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
    3.24    val max_threads_value: unit -> int
    3.25    val max_threads_update: int -> unit
    3.26    val enabled: unit -> bool
    3.27 @@ -75,9 +70,6 @@
    3.28      val _ = Thread.setAttributes orig_atts;
    3.29    in Exn.release result end;
    3.30  
    3.31 -
    3.32 -(* portable wrappers *)
    3.33 -
    3.34  fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
    3.35  
    3.36  fun uninterruptible f x =
    3.37 @@ -179,6 +171,3 @@
    3.38  end;
    3.39  
    3.40  end;
    3.41 -
    3.42 -structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
    3.43 -open Basic_Multithreading;
     4.1 --- a/src/Pure/Concurrent/par_list.ML	Wed Apr 06 16:51:52 2016 +0200
     4.2 +++ b/src/Pure/Concurrent/par_list.ML	Wed Apr 06 17:16:30 2016 +0200
     4.3 @@ -33,7 +33,7 @@
     4.4    if null xs orelse null (tl xs) orelse not (Multithreading.enabled ())
     4.5    then map (Exn.capture f) xs
     4.6    else
     4.7 -    uninterruptible (fn restore_attributes => fn () =>
     4.8 +    Multithreading.uninterruptible (fn restore_attributes => fn () =>
     4.9        let
    4.10          val (group, pri) =
    4.11            (case Future.worker_task () of
     5.1 --- a/src/Pure/Concurrent/single_assignment.ML	Wed Apr 06 16:51:52 2016 +0200
     5.2 +++ b/src/Pure/Concurrent/single_assignment.ML	Wed Apr 06 17:16:30 2016 +0200
     5.3 @@ -48,7 +48,7 @@
     5.4      (case peek v of
     5.5        SOME _ => raise Fail ("Duplicate assignment to " ^ name)
     5.6      | NONE =>
     5.7 -        uninterruptible (fn _ => fn () =>
     5.8 +        Multithreading.uninterruptible (fn _ => fn () =>
     5.9           (SingleAssignment.saset (var, x); ConditionVar.broadcast cond)) ()));
    5.10  
    5.11  end;
     6.1 --- a/src/Pure/Concurrent/synchronized.ML	Wed Apr 06 16:51:52 2016 +0200
     6.2 +++ b/src/Pure/Concurrent/synchronized.ML	Wed Apr 06 17:16:30 2016 +0200
     6.3 @@ -51,7 +51,7 @@
     6.4                | Exn.Res false => NONE
     6.5                | Exn.Exn exn => Exn.reraise exn)
     6.6            | SOME (y, x') =>
     6.7 -              uninterruptible (fn _ => fn () =>
     6.8 +              Multithreading.uninterruptible (fn _ => fn () =>
     6.9                  (var := x'; ConditionVar.broadcast cond; SOME y)) ())
    6.10          end;
    6.11      in try_change () end);
     7.1 --- a/src/Pure/Concurrent/task_queue.ML	Wed Apr 06 16:51:52 2016 +0200
     7.2 +++ b/src/Pure/Concurrent/task_queue.ML	Wed Apr 06 17:16:30 2016 +0200
     7.3 @@ -135,7 +135,7 @@
     7.4  fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
     7.5  
     7.6  fun update_timing update (Task {timing, ...}) e =
     7.7 -  uninterruptible (fn restore_attributes => fn () =>
     7.8 +  Multithreading.uninterruptible (fn restore_attributes => fn () =>
     7.9      let
    7.10        val start = Time.now ();
    7.11        val result = Exn.capture (restore_attributes e) ();
     8.1 --- a/src/Pure/Concurrent/thread_data.ML	Wed Apr 06 16:51:52 2016 +0200
     8.2 +++ b/src/Pure/Concurrent/thread_data.ML	Wed Apr 06 17:16:30 2016 +0200
     8.3 @@ -39,7 +39,8 @@
     8.4  
     8.5  (* thread attributes *)
     8.6  
     8.7 -local
     8.8 +structure Multithreading =
     8.9 +struct
    8.10  
    8.11  val no_interrupts =
    8.12    [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
    8.13 @@ -57,8 +58,6 @@
    8.14      val _ = Thread.setAttributes orig_atts;
    8.15    in Exn.release result end;
    8.16  
    8.17 -in
    8.18 -
    8.19  fun uninterruptible f x =
    8.20    with_attributes no_interrupts (fn atts =>
    8.21      f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
    8.22 @@ -81,7 +80,7 @@
    8.23  fun put (Var tag) data = Thread.setLocal (tag, data);
    8.24  
    8.25  fun setmp v data f x =
    8.26 -  uninterruptible (fn restore_attributes => fn () =>
    8.27 +  Multithreading.uninterruptible (fn restore_attributes => fn () =>
    8.28      let
    8.29        val orig_data = get v;
    8.30        val _ = put v data;
     9.1 --- a/src/Pure/Concurrent/unsynchronized.ML	Wed Apr 06 16:51:52 2016 +0200
     9.2 +++ b/src/Pure/Concurrent/unsynchronized.ML	Wed Apr 06 17:16:30 2016 +0200
     9.3 @@ -19,7 +19,7 @@
     9.4  fun dec i = (i := ! i - (1: int); ! i);
     9.5  
     9.6  fun setmp flag value f x =
     9.7 -  uninterruptible (fn restore_attributes => fn () =>
     9.8 +  Multithreading.uninterruptible (fn restore_attributes => fn () =>
     9.9      let
    9.10        val orig_value = ! flag;
    9.11        val _ = flag := value;
    10.1 --- a/src/Pure/ML/exn_debugger.ML	Wed Apr 06 16:51:52 2016 +0200
    10.2 +++ b/src/Pure/ML/exn_debugger.ML	Wed Apr 06 17:16:30 2016 +0200
    10.3 @@ -42,7 +42,7 @@
    10.4  in
    10.5  
    10.6  fun capture_exception_trace e =
    10.7 -  uninterruptible (fn restore_attributes => fn () =>
    10.8 +  Multithreading.uninterruptible (fn restore_attributes => fn () =>
    10.9      let
   10.10        val _ = start_trace ();
   10.11        val result = Exn.interruptible_capture (restore_attributes e) ();
    11.1 --- a/src/Pure/ML/exn_properties.ML	Wed Apr 06 16:51:52 2016 +0200
    11.2 +++ b/src/Pure/ML/exn_properties.ML	Wed Apr 06 17:16:30 2016 +0200
    11.3 @@ -63,7 +63,7 @@
    11.4                startLine = #startLine loc, endLine = #endLine loc,
    11.5                startPosition = #startPosition loc, endPosition = #endPosition loc};
    11.6          in
    11.7 -          uninterruptible (fn _ => fn () =>
    11.8 +          Multithreading.uninterruptible (fn _ => fn () =>
    11.9              PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
   11.10          end
   11.11      end;
    12.1 --- a/src/Pure/PIDE/execution.ML	Wed Apr 06 16:51:52 2016 +0200
    12.2 +++ b/src/Pure/PIDE/execution.ML	Wed Apr 06 17:16:30 2016 +0200
    12.3 @@ -89,7 +89,7 @@
    12.4  type params = {name: string, pos: Position.T, pri: int};
    12.5  
    12.6  fun fork ({name, pos, pri}: params) e =
    12.7 -  uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
    12.8 +  Multithreading.uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
    12.9      let
   12.10        val exec_id = the_default 0 (Position.parse_id pos);
   12.11        val group = Future.worker_subgroup ();
    13.1 --- a/src/Pure/PIDE/query_operation.ML	Wed Apr 06 16:51:52 2016 +0200
    13.2 +++ b/src/Pure/PIDE/query_operation.ML	Wed Apr 06 17:16:30 2016 +0200
    13.3 @@ -19,7 +19,7 @@
    13.4    Command.print_function (name ^ "_query")
    13.5      (fn {args = instance :: args, ...} =>
    13.6        SOME {delay = NONE, pri = pri, persistent = false, strict = false,
    13.7 -        print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
    13.8 +        print_fn = fn _ => Multithreading.uninterruptible (fn restore_attributes => fn state =>
    13.9            let
   13.10              fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
   13.11              fun status m = output_result (Markup.markup_only m);
    14.1 --- a/src/Pure/System/bash.ML	Wed Apr 06 16:51:52 2016 +0200
    14.2 +++ b/src/Pure/System/bash.ML	Wed Apr 06 17:16:30 2016 +0200
    14.3 @@ -12,7 +12,7 @@
    14.4  structure Bash: BASH =
    14.5  struct
    14.6  
    14.7 -val process = uninterruptible (fn restore_attributes => fn script =>
    14.8 +val process = Multithreading.uninterruptible (fn restore_attributes => fn script =>
    14.9    let
   14.10      datatype result = Wait | Signal | Result of int;
   14.11      val result = Synchronized.var "bash_result" Wait;
    15.1 --- a/src/Pure/System/command_line.ML	Wed Apr 06 16:51:52 2016 +0200
    15.2 +++ b/src/Pure/System/command_line.ML	Wed Apr 06 17:16:30 2016 +0200
    15.3 @@ -14,7 +14,7 @@
    15.4  struct
    15.5  
    15.6  fun tool body =
    15.7 -  uninterruptible (fn restore_attributes => fn () =>
    15.8 +  Multithreading.uninterruptible (fn restore_attributes => fn () =>
    15.9      let
   15.10        val rc =
   15.11          restore_attributes body () handle exn =>
    16.1 --- a/src/Pure/System/isabelle_process.ML	Wed Apr 06 16:51:52 2016 +0200
    16.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Apr 06 17:16:30 2016 +0200
    16.3 @@ -187,7 +187,7 @@
    16.4  val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
    16.5  val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
    16.6  
    16.7 -val init_protocol = uninterruptible (fn _ => fn socket =>
    16.8 +val init_protocol = Multithreading.uninterruptible (fn _ => fn socket =>
    16.9    let
   16.10      val _ = SHA1.test_samples ()
   16.11        handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
    17.1 --- a/src/Pure/System/windows/bash.ML	Wed Apr 06 16:51:52 2016 +0200
    17.2 +++ b/src/Pure/System/windows/bash.ML	Wed Apr 06 17:16:30 2016 +0200
    17.3 @@ -12,7 +12,7 @@
    17.4  structure Bash: BASH =
    17.5  struct
    17.6  
    17.7 -val process = uninterruptible (fn restore_attributes => fn script =>
    17.8 +val process = Multithreading.uninterruptible (fn restore_attributes => fn script =>
    17.9    let
   17.10      datatype result = Wait | Signal | Result of int;
   17.11      val result = Synchronized.var "bash_result" Wait;
    18.1 --- a/src/Pure/Thy/thy_info.ML	Wed Apr 06 16:51:52 2016 +0200
    18.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Apr 06 17:16:30 2016 +0200
    18.3 @@ -185,7 +185,7 @@
    18.4          in result_theory result end
    18.5      | Finished thy => thy)) #> ignore;
    18.6  
    18.7 -val schedule_futures = uninterruptible (fn _ => fn tasks =>
    18.8 +val schedule_futures = Multithreading.uninterruptible (fn _ => fn tasks =>
    18.9    let
   18.10      val futures = tasks
   18.11        |> String_Graph.schedule (fn deps => fn (name, task) =>
    19.1 --- a/src/Pure/Tools/debugger.ML	Wed Apr 06 16:51:52 2016 +0200
    19.2 +++ b/src/Pure/Tools/debugger.ML	Wed Apr 06 17:16:30 2016 +0200
    19.3 @@ -227,7 +227,7 @@
    19.4  in
    19.5  
    19.6  fun debugger_loop thread_name =
    19.7 -  uninterruptible (fn restore_attributes => fn () =>
    19.8 +  Multithreading.uninterruptible (fn restore_attributes => fn () =>
    19.9      let
   19.10        fun loop () =
   19.11          (debugger_state thread_name; if debugger_command thread_name then loop () else ());