src/Pure/PIDE/session.ML
author wenzelm
Thu, 15 Jan 2015 12:54:08 +0100
changeset 59369 7090199d3f78
parent 59345 b02b1fbcf051
child 59445 2c27c3d1fd3b
permissions -rw-r--r--
more informative build_theories_result: cumulative Runtime.exn_message;
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
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    14
  val shutdown: unit -> unit
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48445
diff changeset
    15
  val finish: unit -> unit
59344
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    16
  val save: string -> unit
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    17
  val protocol_handler: string -> unit
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    18
  val init_protocol_handlers: unit -> 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
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    24
(** session identification -- not thread-safe **)
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    25
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    26
val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
32738
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
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    29
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
    30
26109
c69c3559355b more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents: 25840
diff changeset
    31
fun welcome () =
57649
a43898f76ae9 further distinction of Isabelle distribution: alert for identified release candidates;
wenzelm
parents: 56533
diff changeset
    32
  if Distribution.is_identified then
26134
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    33
    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
48990
12814717c95c discontinued centralistic changelog;
wenzelm
parents: 48805
diff changeset
    34
  else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    35
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    36
59086
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    37
(* base syntax *)
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    38
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    39
val keywords = Unsynchronized.ref Keyword.empty_keywords;
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    40
fun get_keywords () = ! keywords;
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    41
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    42
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    43
(* init *)
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    44
56533
cd8b6d849b6a explicit 'document_files' in session ROOT specifications;
wenzelm
parents: 56530
diff changeset
    45
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
    46
    parent (chapter, name) verbose =
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    47
  if #name (! session) <> parent orelse not (! session_finished) then
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    48
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    49
  else
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    50
    let
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    51
      val _ = session := {chapter = chapter, name = name};
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    52
      val _ = session_finished := false;
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    53
    in
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    54
      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
    55
        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
    56
        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
    57
    end;
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
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    60
(* finish *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    61
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    62
fun shutdown () =
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    63
 (Execution.shutdown ();
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    64
  Event_Timer.shutdown ();
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    65
  Future.shutdown ());
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    66
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    67
fun finish () =
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    68
 (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
    69
  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
    70
  Present.finish ();
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    71
  shutdown ();
59086
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    72
  keywords :=
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    73
    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
    74
      (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
    75
  session_finished := true);
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    76
59344
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    77
fun save heap =
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    78
 (shutdown ();
59344
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    79
  ML_System.share_common_data ();
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    80
  ML_System.save_state heap);
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 59086
diff changeset
    81
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    82
56210
c7c85cdb725d clarified module arrangement;
wenzelm
parents: 55386
diff changeset
    83
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    84
(** protocol handlers **)
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
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
    87
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    88
fun protocol_handler name =
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    89
  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
    90
   (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
    91
    if not (member (op =) handlers name) then ()
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    92
    else warning ("Redefining protocol handler: " ^ quote name);
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    93
    update (op =) name handlers));
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    94
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    95
fun init_protocol_handlers () =
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    96
  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
    97
  |> 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
    98
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    99
end;