src/Pure/Isar/session.ML
author berghofe
Tue Jan 11 14:16:30 2005 +0100 (2005-01-11)
changeset 15433 a2cbdf16832e
parent 15269 f856f4f3258f
child 15531 08c8dad8e399
permissions -rw-r--r--
Added flag for hiding proofs in documents to use_dir.
wenzelm@6346
     1
(*  Title:      Pure/Isar/session.ML
wenzelm@6346
     2
    ID:         $Id$
wenzelm@6346
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6346
     4
wenzelm@6346
     5
Session management -- maintain state of logic images.
wenzelm@6346
     6
*)
wenzelm@6346
     7
wenzelm@6346
     8
signature SESSION =
wenzelm@6346
     9
sig
wenzelm@11509
    10
  val name: unit -> string
wenzelm@6346
    11
  val welcome: unit -> string
webertj@15269
    12
  val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string
berghofe@15433
    13
    -> string -> string -> string -> int -> bool -> bool -> unit
wenzelm@6346
    14
  val finish: unit -> unit
wenzelm@6346
    15
end;
wenzelm@6346
    16
wenzelm@6346
    17
structure Session: SESSION =
wenzelm@6346
    18
struct
wenzelm@6346
    19
wenzelm@6346
    20
wenzelm@6346
    21
(* session state *)
wenzelm@6346
    22
wenzelm@6346
    23
val pure = "Pure";
wenzelm@6346
    24
wenzelm@6346
    25
val session = ref ([pure]: string list);
wenzelm@6346
    26
val session_path = ref ([]: string list);
wenzelm@6346
    27
val session_finished = ref false;
wenzelm@9414
    28
val rpath = ref (None: Url.T option);
wenzelm@9414
    29
wenzelm@9414
    30
wenzelm@9414
    31
(* access path *)
wenzelm@6346
    32
wenzelm@6346
    33
fun path () = ! session_path;
wenzelm@6346
    34
wenzelm@10937
    35
fun str_of [] = pure
wenzelm@6346
    36
  | str_of elems = space_implode "/" elems;
wenzelm@6346
    37
wenzelm@11509
    38
fun name () = "Isabelle/" ^ str_of (path ());
wenzelm@11509
    39
fun welcome () = "Welcome to " ^ name () ^ " (" ^ version ^ ")";
wenzelm@6346
    40
wenzelm@6346
    41
wenzelm@9414
    42
(* add_path *)
wenzelm@9414
    43
wenzelm@9414
    44
fun add_path reset s =
wenzelm@9414
    45
  let val sess = ! session @ [s] in
wenzelm@9414
    46
    (case Library.duplicates sess of
wenzelm@9414
    47
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
wenzelm@9414
    48
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
wenzelm@9414
    49
  end;
wenzelm@9414
    50
wenzelm@9414
    51
wenzelm@6346
    52
(* init *)
wenzelm@6346
    53
wenzelm@6346
    54
fun init reset parent name =
wenzelm@6346
    55
  if not (parent mem_string (! session)) orelse not (! session_finished) then
wenzelm@6346
    56
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
wenzelm@6346
    57
  else (add_path reset name; session_finished := false);
wenzelm@6346
    58
wenzelm@6346
    59
wenzelm@6346
    60
(* finish *)
wenzelm@6346
    61
wenzelm@6346
    62
fun finish () =
wenzelm@6663
    63
  (ThyInfo.finish ();
wenzelm@6346
    64
    Present.finish ();
wenzelm@6346
    65
    session_finished := true);
wenzelm@6346
    66
wenzelm@6346
    67
wenzelm@6346
    68
(* use_dir *)
wenzelm@6346
    69
webertj@15269
    70
(*
wenzelm@6346
    71
val root_file = ThyLoad.ml_path "ROOT";
webertj@15269
    72
*)
wenzelm@6346
    73
berghofe@7236
    74
fun get_rpath rpath_str =
berghofe@7236
    75
  (if rpath_str = "" then () else
berghofe@7227
    76
     if is_some (!rpath) then
berghofe@7227
    77
       error "Path for remote theory browsing information may only be set once"
berghofe@7227
    78
     else
berghofe@7227
    79
       rpath := Some (Url.unpack rpath_str);
berghofe@7236
    80
   (!rpath, rpath_str <> ""));
berghofe@7236
    81
berghofe@15433
    82
fun use_dir root_file build modes reset info doc doc_graph parent name dump rpath_str level verbose hide =
wenzelm@11543
    83
  Library.setmp print_mode (modes @ ! print_mode)
berghofe@15433
    84
    (Library.setmp Proofterm.proofs level (Library.setmp IsarOutput.hide_commands hide (fn () =>
wenzelm@11543
    85
      (init reset parent name;
wenzelm@11910
    86
       Present.init build info doc doc_graph (path ()) name
wenzelm@11579
    87
         (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str) verbose;
webertj@15269
    88
       File.use (Path.basic root_file);
berghofe@15433
    89
       finish ())))) ()
wenzelm@10571
    90
  handle exn => (writeln (Toplevel.exn_message exn); exit 1);
wenzelm@6346
    91
wenzelm@6346
    92
wenzelm@6346
    93
end;