src/Pure/System/session.ML
author wenzelm
Wed Jun 02 11:09:26 2010 +0200 (2010-06-02 ago)
changeset 37251 72c7e636067b
parent 37216 3165bc303f66
child 39616 8052101883c3
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
     1 (*  Title:      Pure/System/session.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Session management -- maintain state of logic images.
     5 *)
     6 
     7 signature SESSION =
     8 sig
     9   val id: unit -> string list
    10   val name: unit -> string
    11   val welcome: unit -> string
    12   val use_dir: string -> string -> bool -> string list -> bool -> bool ->
    13     string -> bool -> string list -> string -> string -> bool * string ->
    14     string -> int -> bool -> bool -> int -> int -> int -> unit
    15   val finish: unit -> unit
    16 end;
    17 
    18 structure Session: SESSION =
    19 struct
    20 
    21 
    22 (* session state *)
    23 
    24 val session = Unsynchronized.ref ([Context.PureN]: string list);
    25 val session_path = Unsynchronized.ref ([]: string list);
    26 val session_finished = Unsynchronized.ref false;
    27 val remote_path = Unsynchronized.ref (NONE: Url.T option);
    28 
    29 
    30 (* access path *)
    31 
    32 fun id () = ! session;
    33 fun path () = ! session_path;
    34 
    35 fun str_of [] = Context.PureN
    36   | str_of elems = space_implode "/" elems;
    37 
    38 fun name () = "Isabelle/" ^ str_of (path ());
    39 
    40 
    41 (* welcome *)
    42 
    43 fun welcome () =
    44   if Distribution.is_official then
    45     "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
    46   else
    47     "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^
    48     (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
    49 
    50 val _ =
    51   Outer_Syntax.improper_command "welcome" "print welcome message" Keyword.diag
    52     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
    53 
    54 
    55 (* add_path *)
    56 
    57 fun add_path reset s =
    58   let val sess = ! session @ [s] in
    59     (case duplicates (op =) sess of
    60       [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
    61     | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
    62   end;
    63 
    64 
    65 (* init *)
    66 
    67 fun init reset parent name =
    68   if not (member (op =) (! session) parent) orelse not (! session_finished) then
    69     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    70   else (add_path reset name; session_finished := false);
    71 
    72 
    73 (* finish *)
    74 
    75 fun finish () =
    76   (Thy_Info.finish ();
    77     Present.finish ();
    78     Future.shutdown ();
    79     session_finished := true);
    80 
    81 
    82 (* use_dir *)
    83 
    84 fun get_rpath rpath =
    85   (if rpath = "" then () else
    86      if is_some (! remote_path) then
    87        error "Path for remote theory browsing information may only be set once"
    88      else
    89        remote_path := SOME (Url.explode rpath);
    90    (! remote_path, rpath <> ""));
    91 
    92 fun dumping (_, "") = NONE
    93   | dumping (cp, path) = SOME (cp, Path.explode path);
    94 
    95 fun use_dir item root build modes reset info doc doc_graph doc_versions parent
    96     name dump rpath level timing verbose max_threads trace_threads parallel_proofs =
    97   ((fn () =>
    98      (init reset parent name;
    99       Present.init build info doc doc_graph doc_versions (path ()) name
   100         (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
   101       if timing then
   102         let
   103           val start = start_timing ();
   104           val _ = use root;
   105           val stop = end_timing start;
   106           val _ =
   107             Output.std_error ("Timing " ^ item ^ " (" ^
   108               string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
   109               #message stop ^ ")\n");
   110         in () end
   111       else use root;
   112       finish ()))
   113     |> setmp_noncritical Proofterm.proofs level
   114     |> setmp_noncritical print_mode (modes @ print_mode_value ())
   115     |> setmp_noncritical Goal.parallel_proofs parallel_proofs
   116     |> setmp_noncritical Multithreading.trace trace_threads
   117     |> setmp_noncritical Multithreading.max_threads
   118       (if Multithreading.available then max_threads
   119        else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
   120   handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
   121 
   122 end;