# HG changeset patch
# User wenzelm
# Date 1609766623 -3600
# Node ID e7855739409e7e0bb4f2e7e8b8af0f947823a53e
# Parent  759b6869377d05941e9506569fedbb23eee50d00
tuned signature;

diff -r 759b6869377d -r e7855739409e src/Pure/PIDE/command.ML
--- 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 *)
 
diff -r 759b6869377d -r e7855739409e src/Pure/Thy/thy_info.ML
--- 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