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