src/Pure/System/session.ML
author wenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 48709 719f458cd89e
child 48804 6348e5fca42e
permissions -rw-r--r--
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
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
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    13
  val init: bool -> bool -> bool -> string -> string -> bool -> 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 ^ ")"
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    46
  else
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    47
    "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^
27643
cc13e03124f0 explicit Distribution.changelog;
wenzelm
parents: 26612
diff changeset
    48
    (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    49
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    50
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    51
(* add_path *)
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    52
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    53
fun add_path reset s =
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    54
  let val sess = ! session @ [s] in
18964
67f572e03236 renamed gen_duplicates to duplicates;
wenzelm
parents: 18928
diff changeset
    55
    (case duplicates (op =) sess of
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    56
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
48542
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    57
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups))
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    58
  end;
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    59
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    60
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    61
(* init_name *)
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    62
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    63
fun init_name reset parent name =
20664
ffbc5a57191a member (op =);
wenzelm
parents: 18964
diff changeset
    64
  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
    65
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    66
  else (add_path reset name; session_finished := false);
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
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    69
(* finish *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    70
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    71
fun finish () =
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36953
diff changeset
    72
  (Thy_Info.finish ();
28207
e2431cc4dc66 finish: Future.shutdown last;
wenzelm
parents: 28205
diff changeset
    73
    Present.finish ();
48709
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48698
diff changeset
    74
    Keyword.status ();
46970
9667e0dcb5e2 check declared vs. defined commands at end of session;
wenzelm
parents: 46961
diff changeset
    75
    Outer_Syntax.check_syntax ();
28205
17a81e481142 finish: Future.shutdown;
wenzelm
parents: 27643
diff changeset
    76
    Future.shutdown ();
48698
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48646
diff changeset
    77
    Options.reset_default ();
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    78
    session_finished := true);
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
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    81
(* use_dir *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    82
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    83
fun with_timing _ false f x = f x
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    84
  | with_timing item true f x =
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    85
      let
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    86
        val start = Timing.start ();
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    87
        val y = f x;
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    88
        val timing = Timing.result start;
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    89
        val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    90
          |> Real.fmt (StringCvt.FIX (SOME 2));
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    91
        val _ =
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    92
          Output.physical_stderr ("Timing " ^ item ^ " (" ^
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    93
            string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    94
            Timing.message timing ^ ", factor " ^ factor ^ ")\n");
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    95
      in y end;
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    96
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
    97
fun get_rpath rpath =
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
    98
  (if rpath = "" then () else
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
    99
     if is_some (! remote_path) then
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   100
       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
   101
     else
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   102
       remote_path := SOME (Url.explode rpath);
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   103
   (! remote_path, rpath <> ""));
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   104
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   105
fun init build reset info info_path doc doc_graph doc_variants parent name doc_dump rpath verbose =
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
   106
 (init_name reset parent name;
48467
a4318c36a829 more precise propagation of options: build, session, theories;
wenzelm
parents: 48457
diff changeset
   107
  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   108
    (path ()) name doc_dump (get_rpath rpath) verbose
48467
a4318c36a829 more precise propagation of options: build, session, theories;
wenzelm
parents: 48457
diff changeset
   109
    (map Thy_Info.get_theory (Thy_Info.get_names ())));
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
   110
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   111
local
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   112
48543
93b558e05f21 prefer explicit datatype Present.dump_mode;
wenzelm
parents: 48542
diff changeset
   113
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
   114
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
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 39733
diff changeset
   118
    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
   119
    parallel_proofs parallel_proofs_threshold =
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
   120
  ((fn () =>
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   121
     (init build reset info info_path doc doc_graph doc_variants parent name
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   122
        (doc_dump dump) rpath verbose;
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
   123
      with_timing item timing use root;
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
   124
      finish ()))
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   125
    |> Unsynchronized.setmp Proofterm.proofs level
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   126
    |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   127
    |> 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
   128
    |> 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
   129
    |> Unsynchronized.setmp Multithreading.trace trace_threads
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 37216
diff changeset
   130
    |> Unsynchronized.setmp Multithreading.max_threads
23979
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   131
      (if Multithreading.available then max_threads
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   132
       else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
31478
5e412e4c6546 ML_Compiler.exn_message;
wenzelm
parents: 30173
diff changeset
   133
  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
   134
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
   135
end;
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   136
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48467
diff changeset
   137
end;