src/Pure/System/session.ML
author wenzelm
Thu Oct 18 19:58:30 2012 +0200 (2012-10-18)
changeset 49931 85780e6f8fd2
parent 49911 262c36fd5f26
child 50121 97d2b77313a0
permissions -rw-r--r--
more basic Goal.reset_futures as snapshot of implicit state;
more robust Session.finish_futures: do not cancel here, to allow later Future.map of persistent futures (notably proof terms);
wenzelm@30173
     1
(*  Title:      Pure/System/session.ML
wenzelm@6346
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6346
     3
wenzelm@6346
     4
Session management -- maintain state of logic images.
wenzelm@6346
     5
*)
wenzelm@6346
     6
wenzelm@6346
     7
signature SESSION =
wenzelm@6346
     8
sig
wenzelm@25840
     9
  val id: unit -> string list
wenzelm@11509
    10
  val name: unit -> string
wenzelm@6346
    11
  val welcome: unit -> string
wenzelm@48457
    12
  val finish: unit -> unit
wenzelm@48805
    13
  val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
wenzelm@48543
    14
    string -> string -> string * Present.dump_mode -> string -> bool -> unit
wenzelm@48457
    15
  val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
wenzelm@48445
    16
  val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
wenzelm@31688
    17
    string -> bool -> string list -> string -> string -> bool * string ->
wenzelm@41703
    18
    string -> int -> bool -> bool -> int -> int -> int -> int -> unit
wenzelm@6346
    19
end;
wenzelm@6346
    20
wenzelm@6346
    21
structure Session: SESSION =
wenzelm@6346
    22
struct
wenzelm@6346
    23
wenzelm@6346
    24
(* session state *)
wenzelm@6346
    25
wenzelm@32738
    26
val session = Unsynchronized.ref ([Context.PureN]: string list);
wenzelm@32738
    27
val session_finished = Unsynchronized.ref false;
wenzelm@48542
    28
wenzelm@48542
    29
fun id () = ! session;
wenzelm@48542
    30
fun name () = "Isabelle/" ^ List.last (! session);
wenzelm@9414
    31
wenzelm@9414
    32
wenzelm@9414
    33
(* access path *)
wenzelm@6346
    34
wenzelm@48542
    35
val session_path = Unsynchronized.ref ([]: string list);
wenzelm@48542
    36
val remote_path = Unsynchronized.ref (NONE: Url.T option);
wenzelm@6346
    37
wenzelm@48542
    38
fun path () = ! session_path;
wenzelm@26109
    39
wenzelm@30173
    40
wenzelm@30173
    41
(* welcome *)
wenzelm@30173
    42
wenzelm@26109
    43
fun welcome () =
wenzelm@26134
    44
  if Distribution.is_official then
wenzelm@26134
    45
    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
wenzelm@48990
    46
  else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
wenzelm@6346
    47
wenzelm@6346
    48
wenzelm@9414
    49
(* add_path *)
wenzelm@9414
    50
wenzelm@9414
    51
fun add_path reset s =
wenzelm@9414
    52
  let val sess = ! session @ [s] in
wenzelm@18964
    53
    (case duplicates (op =) sess of
wenzelm@9414
    54
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
wenzelm@48542
    55
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups))
wenzelm@9414
    56
  end;
wenzelm@9414
    57
wenzelm@9414
    58
wenzelm@48457
    59
(* init_name *)
wenzelm@6346
    60
wenzelm@48457
    61
fun init_name reset parent name =
wenzelm@20664
    62
  if not (member (op =) (! session) parent) orelse not (! session_finished) then
wenzelm@6346
    63
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
wenzelm@6346
    64
  else (add_path reset name; session_finished := false);
wenzelm@6346
    65
wenzelm@6346
    66
wenzelm@6346
    67
(* finish *)
wenzelm@6346
    68
wenzelm@49931
    69
fun finish_futures () =
wenzelm@49931
    70
  (case map_filter Task_Queue.group_status (Goal.reset_futures ()) of
wenzelm@49931
    71
    [] => ()
wenzelm@49931
    72
  | exns => raise Par_Exn.make exns);
wenzelm@49931
    73
wenzelm@6346
    74
fun finish () =
wenzelm@49911
    75
 (Future.shutdown ();
wenzelm@49931
    76
  finish_futures ();
wenzelm@49911
    77
  Thy_Info.finish ();
wenzelm@49911
    78
  Present.finish ();
wenzelm@49911
    79
  Keyword.status ();
wenzelm@49911
    80
  Outer_Syntax.check_syntax ();
wenzelm@49911
    81
  Options.reset_default ();
wenzelm@49911
    82
  session_finished := true);
wenzelm@6346
    83
wenzelm@6346
    84
wenzelm@6346
    85
(* use_dir *)
wenzelm@6346
    86
wenzelm@48457
    87
fun with_timing _ false f x = f x
wenzelm@48457
    88
  | with_timing item true f x =
wenzelm@48457
    89
      let
wenzelm@48457
    90
        val start = Timing.start ();
wenzelm@48457
    91
        val y = f x;
wenzelm@48457
    92
        val timing = Timing.result start;
wenzelm@48457
    93
        val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
wenzelm@48457
    94
          |> Real.fmt (StringCvt.FIX (SOME 2));
wenzelm@48457
    95
        val _ =
wenzelm@48457
    96
          Output.physical_stderr ("Timing " ^ item ^ " (" ^
wenzelm@48457
    97
            string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
wenzelm@48457
    98
            Timing.message timing ^ ", factor " ^ factor ^ ")\n");
wenzelm@48457
    99
      in y end;
wenzelm@48457
   100
wenzelm@48516
   101
fun get_rpath rpath =
wenzelm@48516
   102
  (if rpath = "" then () else
wenzelm@48516
   103
     if is_some (! remote_path) then
wenzelm@48516
   104
       error "Path for remote theory browsing information may only be set once"
wenzelm@48516
   105
     else
wenzelm@48516
   106
       remote_path := SOME (Url.explode rpath);
wenzelm@48516
   107
   (! remote_path, rpath <> ""));
wenzelm@48516
   108
wenzelm@48805
   109
fun init build reset info info_path doc doc_graph doc_output doc_variants
wenzelm@48805
   110
    parent name doc_dump rpath verbose =
wenzelm@48457
   111
 (init_name reset parent name;
wenzelm@48805
   112
  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output
wenzelm@48805
   113
    doc_variants (path ()) name doc_dump (get_rpath rpath) verbose
wenzelm@48467
   114
    (map Thy_Info.get_theory (Thy_Info.get_names ())));
wenzelm@48457
   115
wenzelm@48516
   116
local
wenzelm@48516
   117
wenzelm@48543
   118
fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty);
wenzelm@48516
   119
wenzelm@48804
   120
fun read_variants strs =
wenzelm@48804
   121
  rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
wenzelm@48804
   122
  |> filter_out (fn (_, s) => s = "-");
wenzelm@48804
   123
wenzelm@48516
   124
in
wenzelm@48516
   125
wenzelm@48445
   126
fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
wenzelm@41703
   127
    name dump rpath level timing verbose max_threads trace_threads
wenzelm@41703
   128
    parallel_proofs parallel_proofs_threshold =
wenzelm@23972
   129
  ((fn () =>
wenzelm@49911
   130
    let
wenzelm@49911
   131
      val _ =
wenzelm@49911
   132
        Output.physical_stderr
wenzelm@49911
   133
          "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
wenzelm@49911
   134
      val _ =
wenzelm@49911
   135
        init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
wenzelm@49911
   136
          (doc_dump dump) rpath verbose;
wenzelm@49911
   137
      val res1 = (use |> with_timing item timing |> Exn.capture) root;
wenzelm@49911
   138
      val res2 = Exn.capture finish ();
wenzelm@49911
   139
    in ignore (Par_Exn.release_all [res1, res2]) end)
wenzelm@39616
   140
    |> Unsynchronized.setmp Proofterm.proofs level
wenzelm@39616
   141
    |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
wenzelm@39616
   142
    |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
wenzelm@41703
   143
    |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold
wenzelm@39616
   144
    |> Unsynchronized.setmp Multithreading.trace trace_threads
wenzelm@39616
   145
    |> Unsynchronized.setmp Multithreading.max_threads
wenzelm@23979
   146
      (if Multithreading.available then max_threads
wenzelm@23979
   147
       else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
wenzelm@31478
   148
  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
wenzelm@6346
   149
wenzelm@6346
   150
end;
wenzelm@48516
   151
wenzelm@48516
   152
end;