src/Pure/PIDE/session.ML
author wenzelm
Sun, 23 May 2021 23:15:04 +0200
changeset 73776 9f205ca4178a
parent 73523 2cd23d587db9
child 76406 40a365360680
permissions -rw-r--r--
tuned message, e.g. for Pure bootstrap;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56210
c7c85cdb725d clarified module arrangement;
wenzelm
parents: 55386
diff changeset
     1
(*  Title:      Pure/PIDE/session.ML
52052
892061142ba6 discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents: 52050
diff changeset
     2
    Author:     Makarius
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     3
56210
c7c85cdb725d clarified module arrangement;
wenzelm
parents: 55386
diff changeset
     4
Prover session: persistent state of logic image.
6346
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
72640
fffad9ad660e simplified/clarified persistent session information;
wenzelm
parents: 72622
diff changeset
     9
  val init: string -> unit
60081
9fb7b44e3e7e tuned signature;
wenzelm
parents: 59448
diff changeset
    10
  val get_name: unit -> string
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    11
  val welcome: unit -> string
59086
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    12
  val get_keywords: unit -> Keyword.keywords
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    13
  val shutdown: unit -> unit
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    14
  val finish: unit -> unit
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    15
end;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    16
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    17
structure Session: SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    18
struct
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    19
72640
fffad9ad660e simplified/clarified persistent session information;
wenzelm
parents: 72622
diff changeset
    20
(* session name *)
fffad9ad660e simplified/clarified persistent session information;
wenzelm
parents: 72622
diff changeset
    21
fffad9ad660e simplified/clarified persistent session information;
wenzelm
parents: 72622
diff changeset
    22
val session = Synchronized.var "Session.session" "";
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    23
72640
fffad9ad660e simplified/clarified persistent session information;
wenzelm
parents: 72622
diff changeset
    24
fun init name = Synchronized.change session (K name);
48542
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    25
72640
fffad9ad660e simplified/clarified persistent session information;
wenzelm
parents: 72622
diff changeset
    26
fun get_name () = Synchronized.value session;
60081
9fb7b44e3e7e tuned signature;
wenzelm
parents: 59448
diff changeset
    27
73776
9f205ca4178a tuned message, e.g. for Pure bootstrap;
wenzelm
parents: 73523
diff changeset
    28
fun description () = (case get_name () of "" => "Isabelle" | name => "Isabelle/" ^ name);
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
    29
73523
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 72640
diff changeset
    30
fun welcome () = "Welcome to " ^ description () ^ Isabelle_System.isabelle_heading ();
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    31
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    32
59086
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    33
(* base syntax *)
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    34
62928
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    35
val keywords = Synchronized.var "Session.keywords" Keyword.empty_keywords;
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    36
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    37
fun get_keywords () = Synchronized.value keywords;
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    38
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    39
fun update_keywords () =
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    40
  Synchronized.change keywords
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    41
    (K (fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    42
      (Thy_Info.get_names ()) Keyword.empty_keywords));
59086
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    43
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    44
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    45
(* finish *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    46
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    47
fun shutdown () =
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    48
 (Execution.shutdown ();
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    49
  Event_Timer.shutdown ();
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    50
  Future.shutdown ());
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    51
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    52
fun finish () =
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    53
 (shutdown ();
72098
8c547eac8381 more robust treatment of thm_names, with strict check after all theories are loaded;
wenzelm
parents: 71611
diff changeset
    54
  Par_List.map (Global_Theory.get_thm_names o Thy_Info.get_theory) (Thy_Info.get_names ());
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
    55
  Thy_Info.finish ();
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    56
  shutdown ();
72640
fffad9ad660e simplified/clarified persistent session information;
wenzelm
parents: 72622
diff changeset
    57
  update_keywords ());
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    58
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    59
end;