src/Pure/System/session.ML
author wenzelm
Thu, 18 Oct 2012 13:57:27 +0200
changeset 49911 262c36fd5f26
parent 49895 03871053cdba
child 49931 85780e6f8fd2
permissions -rw-r--r--
collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30173
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29435
diff changeset
     1
(*  Title:      Pure/System/session.ML
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     3
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     4
Session management -- maintain state of logic images.
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     5
*)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     6
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     7
signature SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     8
sig
25840
8a84f00f7139 export session id;
wenzelm
parents: 25703
diff changeset
     9
  val id: unit -> string list
11509
d54301357129 export name;
wenzelm
parents: 10937
diff changeset
    10
  val name: unit -> string
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    11
  val welcome: unit -> string
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    12
  val finish: unit -> unit
48805
c3ea910b3581 explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents: 48804
diff changeset
    13
  val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
48543
93b558e05f21 prefer explicit datatype Present.dump_mode;
wenzelm
parents: 48542
diff changeset
    14
    string -> string -> string * Present.dump_mode -> string -> bool -> unit
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    15
  val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
48445
cb4136e4cabf pass ISABELLE_BROWSER_INFO as explicit argument;
wenzelm
parents: 48418
diff changeset
    16
  val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
31688
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
    17
    string -> bool -> string list -> string -> string -> bool * string ->
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 39733
diff changeset
    18
    string -> int -> bool -> bool -> int -> int -> int -> int -> unit
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    19
end;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    20
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    21
structure Session: SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    22
struct
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    23
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    24
(* session state *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    25
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    26
val session = Unsynchronized.ref ([Context.PureN]: string list);
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    27
val session_finished = Unsynchronized.ref false;
48542
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    28
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    29
fun id () = ! session;
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    30
fun name () = "Isabelle/" ^ List.last (! session);
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    31
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    32
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    33
(* access path *)
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    34
48542
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    35
val session_path = Unsynchronized.ref ([]: string list);
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    36
val remote_path = Unsynchronized.ref (NONE: Url.T option);
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    37
48542
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    38
fun path () = ! session_path;
26109
c69c3559355b more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents: 25840
diff changeset
    39
30173
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29435
diff changeset
    40
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29435
diff changeset
    41
(* welcome *)
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29435
diff changeset
    42
26109
c69c3559355b more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents: 25840
diff changeset
    43
fun welcome () =
26134
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    44
  if Distribution.is_official then
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    45
    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
48990
12814717c95c discontinued centralistic changelog;
wenzelm
parents: 48805
diff changeset
    46
  else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    47
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    48
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    49
(* add_path *)
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    50
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    51
fun add_path reset s =
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    52
  let val sess = ! session @ [s] in
18964
67f572e03236 renamed gen_duplicates to duplicates;
wenzelm
parents: 18928
diff changeset
    53
    (case duplicates (op =) sess of
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    54
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
48542
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    55
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups))
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    56
  end;
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    57
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    58
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    59
(* init_name *)
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    60
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    61
fun init_name reset parent name =
20664
ffbc5a57191a member (op =);
wenzelm
parents: 18964
diff changeset
    62
  if not (member (op =) (! session) parent) orelse not (! session_finished) then
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    63
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    64
  else (add_path reset name; session_finished := false);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    65
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    66
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    67
(* finish *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    68
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    69
fun finish () =
49911
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
    70
 (Future.shutdown ();
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
    71
  Goal.finish_futures ();
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
    72
  Thy_Info.finish ();
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
    73
  Present.finish ();
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
    74
  Keyword.status ();
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
    75
  Outer_Syntax.check_syntax ();
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
    76
  Goal.cancel_futures ();
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
    77
  Future.shutdown ();
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
    78
  Options.reset_default ();
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
    79
  session_finished := true);
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    80
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    81
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    82
(* use_dir *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    83
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    84
fun with_timing _ false f x = f x
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    85
  | with_timing item true f x =
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    86
      let
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    87
        val start = Timing.start ();
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    88
        val y = f x;
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    89
        val timing = Timing.result start;
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    90
        val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    91
          |> Real.fmt (StringCvt.FIX (SOME 2));
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    92
        val _ =
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    93
          Output.physical_stderr ("Timing " ^ item ^ " (" ^
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    94
            string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    95
            Timing.message timing ^ ", factor " ^ factor ^ ")\n");
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    96
      in y end;
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    97
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
    98
fun get_rpath rpath =
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
    99
  (if rpath = "" then () else
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   100
     if is_some (! remote_path) then
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   101
       error "Path for remote theory browsing information may only be set once"
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   102
     else
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   103
       remote_path := SOME (Url.explode rpath);
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   104
   (! remote_path, rpath <> ""));
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   105
48805
c3ea910b3581 explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents: 48804
diff changeset
   106
fun init build reset info info_path doc doc_graph doc_output doc_variants
c3ea910b3581 explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents: 48804
diff changeset
   107
    parent name doc_dump rpath verbose =
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
   108
 (init_name reset parent name;
48805
c3ea910b3581 explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents: 48804
diff changeset
   109
  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output
c3ea910b3581 explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents: 48804
diff changeset
   110
    doc_variants (path ()) name doc_dump (get_rpath rpath) verbose
48467
a4318c36a829 more precise propagation of options: build, session, theories;
wenzelm
parents: 48457
diff changeset
   111
    (map Thy_Info.get_theory (Thy_Info.get_names ())));
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
   112
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   113
local
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   114
48543
93b558e05f21 prefer explicit datatype Present.dump_mode;
wenzelm
parents: 48542
diff changeset
   115
fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty);
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   116
48804
6348e5fca42e more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents: 48709
diff changeset
   117
fun read_variants strs =
6348e5fca42e more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents: 48709
diff changeset
   118
  rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
6348e5fca42e more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents: 48709
diff changeset
   119
  |> filter_out (fn (_, s) => s = "-");
6348e5fca42e more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents: 48709
diff changeset
   120
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   121
in
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   122
48445
cb4136e4cabf pass ISABELLE_BROWSER_INFO as explicit argument;
wenzelm
parents: 48418
diff changeset
   123
fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 39733
diff changeset
   124
    name dump rpath level timing verbose max_threads trace_threads
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 39733
diff changeset
   125
    parallel_proofs parallel_proofs_threshold =
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
   126
  ((fn () =>
49911
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
   127
    let
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
   128
      val _ =
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
   129
        Output.physical_stderr
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
   130
          "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
   131
      val _ =
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
   132
        init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
   133
          (doc_dump dump) rpath verbose;
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
   134
      val res1 = (use |> with_timing item timing |> Exn.capture) root;
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
   135
      val res2 = Exn.capture finish ();
262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents: 49895
diff changeset
   136
    in ignore (Par_Exn.release_all [res1, res2]) end)
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   137
    |> Unsynchronized.setmp Proofterm.proofs level
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   138
    |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   139
    |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 39733
diff changeset
   140
    |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   141
    |> Unsynchronized.setmp Multithreading.trace trace_threads
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   142
    |> Unsynchronized.setmp Multithreading.max_threads
23979
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   143
      (if Multithreading.available then max_threads
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   144
       else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
31478
5e412e4c6546 ML_Compiler.exn_message;
wenzelm
parents: 30173
diff changeset
   145
  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
   146
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
   147
end;
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   148
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   149
end;