discontinued body_range (again): does not quite work, because Position.thread_data is plain Toplevel.pos_of only;

--- a/src/Pure/Isar/outer_syntax.ML	Fri Jan 08 16:36:20 2021 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Jan 08 16:59:27 2021 +0100
@@ -222,14 +222,14 @@
 val before_command =
   Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
 
-fun parse_command thy core_range markers =
+fun parse_command thy markers =
   Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
     let
       val keywords = Thy_Header.get_keywords thy;
       val tr0 =
         Toplevel.empty
         |> Toplevel.name name
-        |> Toplevel.positions pos core_range
+        |> Toplevel.position pos
         |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
         |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
       val command_markers =
@@ -263,15 +263,14 @@
     fun parse () =
       filter Token.is_proper span
       |> Source.of_list
-      |> Source.source Token.stopper
-          (Scan.bulk (fn xs => Parse.!!! (parse_command thy core_range markers) xs))
+      |> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy markers) xs))
       |> Source.exhaust;
   in
     (case parse () of
       [tr] => Toplevel.modify_init init tr
-    | [] => Toplevel.ignored full_range
-    | _ => Toplevel.malformed core_range "Exactly one command expected")
-    handle ERROR msg => Toplevel.malformed core_range msg
+    | [] => Toplevel.ignored (#1 full_range)
+    | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
+    handle ERROR msg => Toplevel.malformed (#1 core_range) msg
   end;
 
 fun parse_text thy init pos text =

--- a/src/Pure/Isar/toplevel.ML	Fri Jan 08 16:36:20 2021 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Jan 08 16:59:27 2021 +0100
@@ -33,11 +33,10 @@
   val empty: transition
   val name_of: transition -> string
   val pos_of: transition -> Position.T
-  val body_range_of: transition -> Position.range
   val timing_of: transition -> Time.time
   val type_error: transition -> string
   val name: string -> transition -> transition
-  val positions: Position.T -> Position.range -> transition -> transition
+  val position: Position.T -> transition -> transition
   val markers: Input.source list -> transition -> transition
   val timing: Time.time -> transition -> transition
   val init_theory: (unit -> theory) -> transition -> transition
@@ -48,8 +47,8 @@
   val keep': (bool -> state -> unit) -> transition -> transition
   val keep_proof: (state -> unit) -> transition -> transition
   val is_ignored: transition -> bool
-  val ignored: Position.range -> transition
-  val malformed: Position.range -> string -> transition
+  val ignored: Position.T -> transition
+  val malformed: Position.T -> string -> transition
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
@@ -336,27 +335,24 @@
 
 datatype transition = Transition of
  {name: string,               (*command name*)
-  pos: Position.T,            (*source position: reference point*)
-  body_range: Position.range, (*source position: main body*)
+  pos: Position.T,            (*source position*)
   markers: Input.source list, (*semantic document markers*)
   timing: Time.time,          (*prescient timing information*)
   trans: trans list};         (*primitive transitions (union)*)
 
-fun make_transition (name, pos, body_range, markers, timing, trans) =
-  Transition {name = name, pos = pos, body_range = body_range, markers = markers,
-    timing = timing, trans = trans};
+fun make_transition (name, pos, markers, timing, trans) =
+  Transition {name = name, pos = pos, markers = markers, timing = timing, trans = trans};
 
-fun map_transition f (Transition {name, pos, body_range, markers, timing, trans}) =
-  make_transition (f (name, pos, body_range, markers, timing, trans));
+fun map_transition f (Transition {name, pos, markers, timing, trans}) =
+  make_transition (f (name, pos, markers, timing, trans));
 
-val empty = make_transition ("", Position.none, Position.no_range, [], Time.zeroTime, []);
+val empty = make_transition ("", Position.none, [], Time.zeroTime, []);
 
 
 (* diagnostics *)
 
 fun name_of (Transition {name, ...}) = name;
 fun pos_of (Transition {pos, ...}) = pos;
-fun body_range_of (Transition {body_range, ...}) = body_range;
 fun timing_of (Transition {timing, ...}) = timing;
 
 fun command_msg msg tr =
@@ -369,23 +365,23 @@
 
 (* modify transitions *)
 
-fun name name = map_transition (fn (_, pos, body_range, markers, timing, trans) =>
-  (name, pos, body_range, markers, timing, trans));
+fun name name = map_transition (fn (_, pos, markers, timing, trans) =>
+  (name, pos, markers, timing, trans));
 
-fun positions pos body_range = map_transition (fn (name, _, _, markers, timing, trans) =>
-  (name, pos, body_range, markers, timing, trans));
+fun position pos = map_transition (fn (name, _, markers, timing, trans) =>
+  (name, pos, markers, timing, trans));
 
-fun markers markers = map_transition (fn (name, pos, body_range, _, timing, trans) =>
-  (name, pos, body_range, markers, timing, trans));
+fun markers markers = map_transition (fn (name, pos, _, timing, trans) =>
+  (name, pos, markers, timing, trans));
 
-fun timing timing = map_transition (fn (name, pos, body_range, markers, _, trans) =>
-  (name, pos, body_range, markers, timing, trans));
+fun timing timing = map_transition (fn (name, pos, markers, _, trans) =>
+  (name, pos, markers, timing, trans));
 
-fun add_trans tr = map_transition (fn (name, pos, body_range, markers, timing, trans) =>
-  (name, pos, body_range, markers, timing, tr :: trans));
+fun add_trans tr = map_transition (fn (name, pos, markers, timing, trans) =>
+  (name, pos, markers, timing, tr :: trans));
 
-val reset_trans = map_transition (fn (name, pos, body_range, markers, timing, _) =>
-  (name, pos, body_range, markers, timing, []));
+val reset_trans = map_transition (fn (name, pos, markers, timing, _) =>
+  (name, pos, markers, timing, []));
 
 
 (* basic transitions *)
@@ -414,11 +410,11 @@
 
 fun is_ignored tr = name_of tr = "<ignored>";
 
-fun ignored range =
-  empty |> name "<ignored>" |> positions (#1 range) range |> keep (fn _ => ());
+fun ignored pos =
+  empty |> name "<ignored>" |> position pos |> keep (fn _ => ());
 
-fun malformed range msg =
-  empty |> name "<malformed>" |> positions (#1 range) range |> keep (fn _ => error msg);
+fun malformed pos msg =
+  empty |> name "<malformed>" |> position pos |> keep (fn _ => error msg);
 
 
 (* theory transitions *)
@@ -598,9 +594,9 @@
 
 (* runtime position *)
 
-fun exec_id id (tr as Transition {pos, body_range, ...}) =
+fun exec_id id (tr as Transition {pos, ...}) =
   let val put_id = Position.put_id (Document_ID.print id)
-  in positions (put_id pos) (apply2 put_id body_range) tr end;
+  in position (put_id pos) tr end;
 
 fun setmp_thread_position (Transition {pos, ...}) f x =
   Position.setmp_thread_data pos f x;

--- a/src/Pure/PIDE/command.ML	Fri Jan 08 16:36:20 2021 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Jan 08 16:59:27 2021 +0100
@@ -156,7 +156,7 @@
         Position.here_list verbatim);
   in
     if exists #1 token_reports
-    then Toplevel.malformed (Token.core_range_of span) "Malformed command syntax"
+    then Toplevel.malformed (#1 (Token.core_range_of span)) "Malformed command syntax"
     else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span)
   end;