src/Pure/PIDE/session.ML
author wenzelm
Sat, 09 Apr 2016 20:18:15 +0200
changeset 62936 72e3811dad76
parent 62928 0953dec1fcb0
child 62944 3ee643c5ed00
permissions -rw-r--r--
avoid interference with running PIDE protocol;
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
60081
9fb7b44e3e7e tuned signature;
wenzelm
parents: 59448
diff changeset
     9
  val get_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
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 60081
diff changeset
    12
  val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
59445
2c27c3d1fd3b provide session_graph.pdf via Isabelle/Scala;
wenzelm
parents: 59369
diff changeset
    13
    (Path.T * Path.T) list -> Path.T -> 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
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
62928
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    23
(** persistent session information **)
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    24
62928
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    25
val session = Synchronized.var "Session.session" ({chapter = "Pure", name = "Pure"}, false);
48542
0a5f598cacec simplified Session.name;
wenzelm
parents: 48518
diff changeset
    26
62928
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    27
fun get_name () = #name (#1 (Synchronized.value session));
60081
9fb7b44e3e7e tuned signature;
wenzelm
parents: 59448
diff changeset
    28
9fb7b44e3e7e tuned signature;
wenzelm
parents: 59448
diff changeset
    29
fun description () = "Isabelle/" ^ get_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
    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
60081
9fb7b44e3e7e tuned signature;
wenzelm
parents: 59448
diff changeset
    33
    "Welcome to " ^ description () ^ " (" ^ Distribution.version ^ ")"
9fb7b44e3e7e tuned signature;
wenzelm
parents: 59448
diff changeset
    34
  else "Unofficial version of " ^ description () ^ " (" ^ 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
62928
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    39
val keywords = Synchronized.var "Session.keywords" Keyword.empty_keywords;
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    40
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    41
fun get_keywords () = Synchronized.value keywords;
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    42
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    43
fun update_keywords () =
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    44
  Synchronized.change keywords
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    45
    (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
    46
      (Thy_Info.get_names ()) Keyword.empty_keywords));
59086
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    47
94b2690ad494 node-specific keywords, with session base syntax as default;
wenzelm
parents: 58928
diff changeset
    48
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 51398
diff changeset
    49
(* init *)
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    50
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 60081
diff changeset
    51
fun init symbols build info info_path doc doc_output doc_variants doc_files graph_file
56530
5c178501cf78 removed obsolete doc_dump option (see also 892061142ba6);
wenzelm
parents: 56333
diff changeset
    52
    parent (chapter, name) verbose =
62928
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    53
  (Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) =>
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    54
    if parent_name <> parent orelse not parent_finished then
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    55
      error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    56
    else ({chapter = chapter, name = name}, false));
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    57
    Present.init symbols build info info_path (if doc = "false" then "" else doc)
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    58
      doc_output doc_variants doc_files graph_file (chapter, name) verbose);
6346
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
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    61
(* finish *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    62
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    63
fun shutdown () =
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    64
 (Execution.shutdown ();
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    65
  Event_Timer.shutdown ();
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    66
  Future.shutdown ());
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    67
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    68
fun finish () =
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    69
 (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
    70
  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
    71
  Present.finish ();
59369
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents: 59345
diff changeset
    72
  shutdown ();
62928
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    73
  update_keywords ();
0953dec1fcb0 prefer Synchronized.var;
wenzelm
parents: 62469
diff changeset
    74
  Synchronized.change session (apsnd (K true)));
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    75
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    76
56210
c7c85cdb725d clarified module arrangement;
wenzelm
parents: 55386
diff changeset
    77
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    78
(** protocol handlers **)
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    79
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    80
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
    81
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    82
fun protocol_handler name =
62936
72e3811dad76 avoid interference with running PIDE protocol;
wenzelm
parents: 62928
diff changeset
    83
  if Thread_Data.is_virtual then ()
72e3811dad76 avoid interference with running PIDE protocol;
wenzelm
parents: 62928
diff changeset
    84
  else
72e3811dad76 avoid interference with running PIDE protocol;
wenzelm
parents: 62928
diff changeset
    85
    Synchronized.change protocol_handlers (fn handlers =>
72e3811dad76 avoid interference with running PIDE protocol;
wenzelm
parents: 62928
diff changeset
    86
     (Output.try_protocol_message (Markup.protocol_handler name) [];
72e3811dad76 avoid interference with running PIDE protocol;
wenzelm
parents: 62928
diff changeset
    87
      if not (member (op =) handlers name) then ()
72e3811dad76 avoid interference with running PIDE protocol;
wenzelm
parents: 62928
diff changeset
    88
      else warning ("Redefining protocol handler: " ^ quote name);
72e3811dad76 avoid interference with running PIDE protocol;
wenzelm
parents: 62928
diff changeset
    89
      update (op =) name handlers));
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    90
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 52083
diff changeset
    91
fun init_protocol_handlers () =
62936
72e3811dad76 avoid interference with running PIDE protocol;
wenzelm
parents: 62928
diff changeset
    92
  if Thread_Data.is_virtual then ()
72e3811dad76 avoid interference with running PIDE protocol;
wenzelm
parents: 62928
diff changeset
    93
  else
72e3811dad76 avoid interference with running PIDE protocol;
wenzelm
parents: 62928
diff changeset
    94
    Synchronized.value protocol_handlers
72e3811dad76 avoid interference with running PIDE protocol;
wenzelm
parents: 62928
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;