--- a/src/Pure/PIDE/command.ML Mon Jan 04 13:40:16 2021 +0100
+++ b/src/Pure/PIDE/command.ML Mon Jan 04 14:23:43 2021 +0100
@@ -11,6 +11,8 @@
val read_thy: Toplevel.state -> theory
val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
blob Exn.result list * int -> Token.T list -> Toplevel.transition
+ val read_span: Keyword.keywords -> Toplevel.state -> Path.T -> (unit -> theory) ->
+ Command_Span.span -> Toplevel.transition
type eval
val eval_command_id: eval -> Document_ID.command
val eval_exec_id: eval -> Document_ID.exec
@@ -166,6 +168,9 @@
end;
+fun read_span keywords st master_dir init =
+ Command_Span.content #> read keywords (read_thy st) master_dir init ([], ~1);
+
(* eval *)
--- a/src/Pure/Thy/thy_info.ML Mon Jan 04 13:40:16 2021 +0100
+++ b/src/Pure/Thy/thy_info.ML Mon Jan 04 14:23:43 2021 +0100
@@ -274,10 +274,9 @@
fun excursion keywords master_dir init elements =
let
- fun prepare_span st span =
- Command_Span.content span
- |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
- |> (fn tr => Toplevel.timing (Resources.last_timing tr) tr);
+ fun prepare_span st =
+ Command.read_span keywords st master_dir init
+ #> (fn tr => Toplevel.timing (Resources.last_timing tr) tr);
fun element_result span_elem (st, _) =
let