src/Pure/System/session.ML
author wenzelm
Mon, 11 Mar 2013 14:25:14 +0100
changeset 51398 c3d02b3518c2
parent 51276 05522141d244
child 51399 6ac3c29a300e
permissions -rw-r--r--
discontinued "isabelle usedir" option -P (remote path);
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 ->
51398
c3d02b3518c2 discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents: 51276
diff changeset
    15
    string -> string -> bool * 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);
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 () =
51276
05522141d244 more explicit Goal.shutdown_futures;
wenzelm
parents: 51045
diff changeset
    70
 (Goal.shutdown_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
    71
  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
    72
  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
    73
  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
    74
  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
    75
  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
    76
  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
    77
  session_finished := true);
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    78
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    79
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    80
(* use_dir *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    81
50777
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    82
fun with_timing name verbose f x =
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    83
  let
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    84
    val start = Timing.start ();
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    85
    val y = f x;
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    86
    val timing = Timing.result start;
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    87
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    88
    val threads = string_of_int (Multithreading.max_threads_value ());
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    89
    val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    90
      |> Real.fmt (StringCvt.FIX (SOME 2));
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    91
51045
630c0895d9d1 more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents: 50781
diff changeset
    92
    val timing_props =
630c0895d9d1 more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents: 50781
diff changeset
    93
      [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
630c0895d9d1 more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents: 50781
diff changeset
    94
    val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props));
50777
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    95
    val _ =
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    96
      if verbose then
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    97
        Output.physical_stderr ("Timing " ^ name ^ " (" ^
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    98
          threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
    99
      else ();
20126dd9772c include timing properties in log;
wenzelm
parents: 50707
diff changeset
   100
  in y end;
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
   101
48805
c3ea910b3581 explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents: 48804
diff changeset
   102
fun init build reset info info_path doc doc_graph doc_output doc_variants
51398
c3d02b3518c2 discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents: 51276
diff changeset
   103
    parent name doc_dump verbose =
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
   104
 (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
   105
  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output
51398
c3d02b3518c2 discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents: 51276
diff changeset
   106
    doc_variants (path ()) name doc_dump verbose
48467
a4318c36a829 more precise propagation of options: build, session, theories;
wenzelm
parents: 48457
diff changeset
   107
    (map Thy_Info.get_theory (Thy_Info.get_names ())));
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
local
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   110
48804
6348e5fca42e more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents: 48709
diff changeset
   111
fun read_variants strs =
6348e5fca42e more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents: 48709
diff changeset
   112
  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
   113
  |> filter_out (fn (_, s) => s = "-");
6348e5fca42e more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents: 48709
diff changeset
   114
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   115
in
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   116
48445
cb4136e4cabf pass ISABELLE_BROWSER_INFO as explicit argument;
wenzelm
parents: 48418
diff changeset
   117
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
   118
    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
   119
    parallel_proofs parallel_proofs_threshold =
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
   120
  ((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
   121
    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
   122
      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
   123
        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
   124
          "### 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
   125
      val _ =
51398
c3d02b3518c2 discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents: 51276
diff changeset
   126
        if rpath = "" then ()
c3d02b3518c2 discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents: 51276
diff changeset
   127
        else
c3d02b3518c2 discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents: 51276
diff changeset
   128
          Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n";
c3d02b3518c2 discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents: 51276
diff changeset
   129
c3d02b3518c2 discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents: 51276
diff changeset
   130
      val _ =
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
   131
        init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
51398
c3d02b3518c2 discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents: 51276
diff changeset
   132
          doc_dump 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
   133
      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
   134
      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
   135
    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
   136
    |> Unsynchronized.setmp Proofterm.proofs level
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   137
    |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   138
    |> 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
   139
    |> 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
   140
    |> Unsynchronized.setmp Multithreading.trace trace_threads
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   141
    |> Unsynchronized.setmp Multithreading.max_threads
23979
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   142
      (if Multithreading.available then max_threads
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   143
       else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
31478
5e412e4c6546 ML_Compiler.exn_message;
wenzelm
parents: 30173
diff changeset
   144
  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
   145
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
   146
end;
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   147
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   148
end;