src/Pure/System/session.ML
author wenzelm
Thu, 24 Jan 2013 17:18:13 +0100
changeset 51045 630c0895d9d1
parent 50781 a0f22c2d60cc
child 51276 05522141d244
permissions -rw-r--r--
more efficient inlined properties, especially relevant for voluminous tasks trace;
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
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents: 50430
diff changeset
    11
  val path: unit -> string list
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    12
  val welcome: unit -> string
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    13
  val finish: unit -> unit
48805
c3ea910b3581 explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents: 48804
diff changeset
    14
  val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
50121
97d2b77313a0 isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
wenzelm
parents: 49931
diff changeset
    15
    string -> string -> bool * string -> string -> bool -> unit
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    16
  val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
48445
cb4136e4cabf pass ISABELLE_BROWSER_INFO as explicit argument;
wenzelm
parents: 48418
diff changeset
    17
  val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
31688
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
    18
    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
    19
    string -> int -> bool -> bool -> int -> int -> int -> int -> unit
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    20
end;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    21
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    22
structure Session: SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    23
struct
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    24
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    25
(* session state *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    26
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    27
val session = Unsynchronized.ref ([Context.PureN]: string list);
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    28
val session_finished = Unsynchronized.ref false;
48542
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    29
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    30
fun id () = ! session;
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    31
fun name () = "Isabelle/" ^ List.last (! session);
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    32
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    33
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    34
(* access path *)
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    35
48542
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    36
val session_path = Unsynchronized.ref ([]: string list);
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    37
val remote_path = Unsynchronized.ref (NONE: Url.T option);
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    38
48542
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    39
fun path () = ! session_path;
26109
c69c3559355b more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents: 25840
diff changeset
    40
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
    41
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
(* 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
    43
26109
c69c3559355b more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents: 25840
diff changeset
    44
fun welcome () =
26134
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    45
  if Distribution.is_official then
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    46
    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
48990
12814717c95c discontinued centralistic changelog;
wenzelm
parents: 48805
diff changeset
    47
  else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    48
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    49
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    50
(* add_path *)
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    51
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    52
fun add_path reset s =
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    53
  let val sess = ! session @ [s] in
18964
67f572e03236 renamed gen_duplicates to duplicates;
wenzelm
parents: 18928
diff changeset
    54
    (case duplicates (op =) sess of
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    55
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
48542
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    56
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups))
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    57
  end;
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    58
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    59
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    60
(* init_name *)
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    61
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    62
fun init_name reset parent name =
20664
ffbc5a57191a member (op =);
wenzelm
parents: 18964
diff changeset
    63
  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
    64
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    65
  else (add_path reset name; session_finished := false);
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
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    68
(* finish *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    69
49931
85780e6f8fd2 more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents: 49911
diff changeset
    70
fun finish_futures () =
85780e6f8fd2 more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents: 49911
diff changeset
    71
  (case map_filter Task_Queue.group_status (Goal.reset_futures ()) of
85780e6f8fd2 more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents: 49911
diff changeset
    72
    [] => ()
85780e6f8fd2 more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents: 49911
diff changeset
    73
  | exns => raise Par_Exn.make exns);
85780e6f8fd2 more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents: 49911
diff changeset
    74
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    75
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
    76
 (Future.shutdown ();
49931
85780e6f8fd2 more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents: 49911
diff changeset
    77
  finish_futures ();
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
    78
  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
    79
  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
    80
  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
    81
  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
    82
  Options.reset_default ();
50430
702278df3b57 make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);
wenzelm
parents: 50121
diff changeset
    83
  Future.shutdown ();
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
    84
  session_finished := true);
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    85
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    86
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    87
(* use_dir *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    88
50777
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    89
fun with_timing name verbose f x =
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    90
  let
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    91
    val start = Timing.start ();
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    92
    val y = f x;
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    93
    val timing = Timing.result start;
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    94
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    95
    val threads = string_of_int (Multithreading.max_threads_value ());
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    96
    val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    97
      |> Real.fmt (StringCvt.FIX (SOME 2));
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    98
51045
630c0895d9d1 more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents: 50781
diff changeset
    99
    val timing_props =
630c0895d9d1 more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents: 50781
diff changeset
   100
      [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
630c0895d9d1 more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents: 50781
diff changeset
   101
    val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props));
50777
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
   102
    val _ =
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
   103
      if verbose then
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
   104
        Output.physical_stderr ("Timing " ^ name ^ " (" ^
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
   105
          threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
   106
      else ();
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
   107
  in y end;
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
   108
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   109
fun get_rpath rpath =
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   110
  (if rpath = "" then () else
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   111
     if is_some (! remote_path) then
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   112
       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
   113
     else
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   114
       remote_path := SOME (Url.explode rpath);
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   115
   (! remote_path, rpath <> ""));
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   116
48805
c3ea910b3581 explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents: 48804
diff changeset
   117
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
   118
    parent name doc_dump rpath verbose =
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
   119
 (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
   120
  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
   121
    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
   122
    (map Thy_Info.get_theory (Thy_Info.get_names ())));
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
   123
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   124
local
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   125
48804
6348e5fca42e more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents: 48709
diff changeset
   126
fun read_variants strs =
6348e5fca42e more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents: 48709
diff changeset
   127
  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
   128
  |> filter_out (fn (_, s) => s = "-");
6348e5fca42e more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents: 48709
diff changeset
   129
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   130
in
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   131
48445
cb4136e4cabf pass ISABELLE_BROWSER_INFO as explicit argument;
wenzelm
parents: 48418
diff changeset
   132
fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
50121
97d2b77313a0 isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
wenzelm
parents: 49931
diff changeset
   133
    name doc_dump rpath level timing verbose max_threads trace_threads
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 39733
diff changeset
   134
    parallel_proofs parallel_proofs_threshold =
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
   135
  ((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
   136
    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
   137
      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
   138
        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
   139
          "### 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
   140
      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
   141
        init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
50121
97d2b77313a0 isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
wenzelm
parents: 49931
diff changeset
   142
          doc_dump rpath verbose;
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
   143
      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
   144
      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
   145
    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
   146
    |> Unsynchronized.setmp Proofterm.proofs level
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   147
    |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   148
    |> 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
   149
    |> 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
   150
    |> Unsynchronized.setmp Multithreading.trace trace_threads
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   151
    |> Unsynchronized.setmp Multithreading.max_threads
23979
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   152
      (if Multithreading.available then max_threads
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   153
       else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
31478
5e412e4c6546 ML_Compiler.exn_message;
wenzelm
parents: 30173
diff changeset
   154
  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
   155
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
   156
end;
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   157
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   158
end;