src/Pure/PIDE/session.ML
author wenzelm
Sat, 10 Jan 2015 21:39:49 +0100
changeset 59345 b02b1fbcf051
parent 59344 e0ce214303c1
child 59369 7090199d3f78
permissions -rw-r--r--
tuned -- less redundant;
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
11509
d54301357129 export name;
wenzelm
parents: 10937
diff changeset
     9
  val name: unit -> string
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    10
  val welcome: unit -> string
59086
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    11
  val get_keywords: unit -> Keyword.keywords
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    12
  val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56530
diff changeset
    13
    (Path.T * Path.T) list -> string -> string * string -> bool -> unit
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    14
  val finish: unit -> unit
59344
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    15
  val save: string -> unit
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    16
  val protocol_handler: string -> unit
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    17
  val init_protocol_handlers: unit -> unit
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    18
end;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    19
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    20
structure Session: SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    21
struct
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    22
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    23
(** session identification -- not thread-safe **)
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    24
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    25
val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    26
val session_finished = Unsynchronized.ref false;
48542
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    27
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    28
fun name () = "Isabelle/" ^ #name (! session);
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
26109
c69c3559355b more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents: 25840
diff changeset
    30
fun welcome () =
57649
a43898f76ae9 further distinction of Isabelle distribution: alert for identified release candidates;
wenzelm
parents: 56533
diff changeset
    31
  if Distribution.is_identified then
26134
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    32
    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
48990
12814717c95c discontinued centralistic changelog;
wenzelm
parents: 48805
diff changeset
    33
  else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    34
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    35
59086
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    36
(* base syntax *)
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    37
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    38
val keywords = Unsynchronized.ref Keyword.empty_keywords;
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    39
fun get_keywords () = ! keywords;
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    40
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    41
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    42
(* init *)
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    43
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56530
diff changeset
    44
fun init build info info_path doc doc_graph doc_output doc_variants doc_files
56530
5c178501cf78 removed obsolete doc_dump option (see also 892061142ba6);
wenzelm
parents: 56333
diff changeset
    45
    parent (chapter, name) verbose =
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    46
  if #name (! session) <> parent orelse not (! session_finished) then
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    47
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    48
  else
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    49
    let
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    50
      val _ = session := {chapter = chapter, name = name};
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    51
      val _ = session_finished := false;
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    52
    in
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    53
      Present.init build info info_path (if doc = "false" then "" else doc)
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56530
diff changeset
    54
        doc_graph doc_output doc_variants doc_files (chapter, name)
56530
5c178501cf78 removed obsolete doc_dump option (see also 892061142ba6);
wenzelm
parents: 56333
diff changeset
    55
        verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    56
    end;
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    57
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
(* finish *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    60
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    61
fun finish () =
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52440
diff changeset
    62
 (Execution.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
    63
  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
    64
  Present.finish ();
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
    65
  Future.shutdown ();
52050
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents: 51948
diff changeset
    66
  Event_Timer.shutdown ();
55386
0c15ac6edcf7 make triple-sure that the future scheduler is properly shutdown (see also 702278df3b57);
wenzelm
parents: 53192
diff changeset
    67
  Future.shutdown ();
59086
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    68
  keywords :=
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    69
    fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    70
      (Thy_Info.get_names ()) Keyword.empty_keywords;
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
  session_finished := true);
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    72
59344
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    73
fun save heap =
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    74
 (Execution.shutdown ();
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    75
  Event_Timer.shutdown ();
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    76
  Future.shutdown ();
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    77
  ML_System.share_common_data ();
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    78
  ML_System.save_state heap);
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    79
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    80
56210
c7c85cdb725d clarified module arrangement;
wenzelm
parents: 55386
diff changeset
    81
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    82
(** protocol handlers **)
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    83
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    84
val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    85
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    86
fun protocol_handler name =
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    87
  Synchronized.change protocol_handlers (fn handlers =>
56333
38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents: 56210
diff changeset
    88
   (Output.try_protocol_message (Markup.protocol_handler name) [];
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    89
    if not (member (op =) handlers name) then ()
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    90
    else warning ("Redefining protocol handler: " ^ quote name);
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    91
    update (op =) name handlers));
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    92
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    93
fun init_protocol_handlers () =
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    94
  Synchronized.value protocol_handlers
56333
38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents: 56210
diff changeset
    95
  |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) []);
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    96
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    97
end;