--- a/src/Pure/Isar/toplevel.ML Mon Feb 27 17:17:26 2017 +0000
+++ b/src/Pure/Isar/toplevel.ML Mon Feb 27 20:44:25 2017 +0100
@@ -75,8 +75,8 @@
val exec_id: Document_ID.exec -> transition -> transition
val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
val add_hook: (transition -> state -> state -> unit) -> unit
- val get_timing: transition -> Time.time option
- val put_timing: Time.time option -> transition -> transition
+ val get_timing: transition -> Time.time
+ val put_timing: Time.time -> transition -> transition
val transition: bool -> transition -> state -> state * (exn * string) option
val command_errors: bool -> transition -> state -> Runtime.error list * state option
val command_exception: bool -> transition -> state -> state
@@ -286,7 +286,7 @@
datatype transition = Transition of
{name: string, (*command name*)
pos: Position.T, (*source position*)
- timing: Time.time option, (*prescient timing information*)
+ timing: Time.time, (*prescient timing information*)
trans: trans list}; (*primitive transitions (union)*)
fun make_transition (name, pos, timing, trans) =
@@ -295,7 +295,7 @@
fun map_transition f (Transition {name, pos, timing, trans}) =
make_transition (f (name, pos, timing, trans));
-val empty = make_transition ("", Position.none, NONE, []);
+val empty = make_transition ("", Position.none, Time.zeroTime, []);
(* diagnostics *)
@@ -649,18 +649,12 @@
val put_result = Proof.map_context o Result.put;
fun timing_estimate include_head elem =
- let
- val trs = Thy_Syntax.flat_element elem |> not include_head ? tl;
- val timings = map get_timing trs;
- in
- if forall is_some timings then
- SOME (fold (curry (op +) o the) timings Time.zeroTime)
- else NONE
- end;
+ let val trs = Thy_Syntax.flat_element elem |> not include_head ? tl
+ in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
-fun priority NONE = ~1
- | priority (SOME estimate) =
- Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
+fun priority estimate =
+ if estimate = Time.zeroTime then ~1
+ else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
fun proof_future_enabled estimate st =
(case try proof_of st of
@@ -669,10 +663,7 @@
not (Proof.is_relevant state) andalso
(if can (Proof.assert_bottom true) state
then Goal.future_enabled 1
- else
- (case estimate of
- NONE => Goal.future_enabled 2
- | SOME t => Goal.future_enabled_timing t)));
+ else Goal.future_enabled 2 orelse Goal.future_enabled_timing estimate));
fun atom_result keywords tr st =
let
--- a/src/Pure/PIDE/resources.ML Mon Feb 27 17:17:26 2017 +0000
+++ b/src/Pure/PIDE/resources.ML Mon Feb 27 20:44:25 2017 +0100
@@ -17,7 +17,7 @@
val provide_parse_files: string -> (theory -> Token.file list * theory) parser
val loaded_files_current: theory -> bool
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
- val load_thy: bool -> HTML.symbols -> (Toplevel.transition -> Time.time option) -> int ->
+ val load_thy: bool -> HTML.symbols -> (Toplevel.transition -> Time.time) -> int ->
Path.T -> Thy_Header.header -> Position.T -> string -> theory list ->
theory * (unit -> unit) * int
end;
--- a/src/Pure/Thy/thy_info.ML Mon Feb 27 17:17:26 2017 +0000
+++ b/src/Pure/Thy/thy_info.ML Mon Feb 27 20:44:25 2017 +0100
@@ -16,7 +16,7 @@
val use_theories:
{document: bool,
symbols: HTML.symbols,
- last_timing: Toplevel.transition -> Time.time option,
+ last_timing: Toplevel.transition -> Time.time,
master_dir: Path.T} -> (string * Position.T) list -> unit
val use_thys: (string * Position.T) list -> unit
val use_thy: string * Position.T -> unit
@@ -350,7 +350,8 @@
val use_thys =
use_theories
- {document = false, symbols = HTML.no_symbols, last_timing = K NONE, master_dir = Path.current};
+ {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
+ master_dir = Path.current};
val use_thy = use_thys o single;
--- a/src/Pure/Tools/build.ML Mon Feb 27 17:17:26 2017 +0000
+++ b/src/Pure/Tools/build.ML Mon Feb 27 20:44:25 2017 +0100
@@ -31,7 +31,7 @@
if name = "" then NONE else SOME {file = file, offset = offset, name = name}
| _ => NONE);
-fun lookup_timings timings tr =
+fun get_timings timings tr =
(case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of
SOME {file, offset, name} =>
(case Symtab.lookup timings file of
@@ -40,7 +40,8 @@
SOME (name', time) => if name = name' then SOME time else NONE
| NONE => NONE)
| NONE => NONE)
- | NONE => NONE);
+ | NONE => NONE)
+ |> the_default Time.zeroTime;
(* session timing *)
@@ -161,7 +162,7 @@
parent_name (chapter, name)
verbose;
- val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
+ val last_timing = get_timings (fold update_timings command_timings empty_timings);
val res1 =
theories |>
@@ -191,8 +192,10 @@
let open XML.Decode
in list (pair Options.decode (list (string #> rpair Position.none))) end;
val res1 =
- Exn.capture (fn () =>
- theories |> List.app (build_theories symbols (K NONE) (Path.explode master_dir))) ();
+ Exn.capture
+ (fn () =>
+ theories
+ |> List.app (build_theories symbols (K Time.zeroTime) (Path.explode master_dir))) ();
val res2 = Exn.capture Session.shutdown ();
val result =
(Par_Exn.release_all [res1, res2]; "") handle exn =>
--- a/src/Tools/VSCode/README.md Mon Feb 27 17:17:26 2017 +0000
+++ b/src/Tools/VSCode/README.md Mon Feb 27 20:44:25 2017 +0100
@@ -42,6 +42,7 @@
* https://code.visualstudio.com/docs/extensionAPI/extension-points
* https://code.visualstudio.com/docs/extensions/example-language-server
* https://github.com/Microsoft/vscode-languageserver-node-example
+* https://github.com/Microsoft/vscode
### Protocol ###
@@ -56,6 +57,7 @@
### Similar projects ###
+* Lean Prover: https://github.com/leanprover/vscode-lean
* Coq: https://github.com/siegebell/vscoq
* OCaml: https://github.com/freebroccolo/vscode-reasonml
* Scala: https://github.com/dragos/dragos-vscode-scala