# HG changeset patch
# User wenzelm
# Date 1610113204 -3600
# Node ID 8a20737e4ebff5a3cab89c568a1e0afbbc1500bc
# Parent  e700ede0038fd813715943b2ad6d7dc344e32b91
support more command positions, analogous to Command.core_range in Isabelle/Scala;

diff -r e700ede0038f -r 8a20737e4ebf src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Jan 08 14:29:58 2021 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Jan 08 14:40:04 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 markers =
+fun parse_command thy core_range 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.position pos
+        |> Toplevel.positions pos core_range
         |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
         |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
       val command_markers =
@@ -256,21 +256,22 @@
 
 fun parse_span thy init span =
   let
-    val range = Token.range_of span;
+    val full_range = Token.range_of span;
     val core_range = Token.core_range_of span;
 
     val markers = map Token.input_of (filter Token.is_document_marker span);
     fun parse () =
       filter Token.is_proper span
       |> Source.of_list
-      |> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy markers) xs))
+      |> Source.source Token.stopper
+          (Scan.bulk (fn xs => Parse.!!! (parse_command thy core_range markers) xs))
       |> Source.exhaust;
   in
     (case parse () of
       [tr] => Toplevel.modify_init init tr
-    | [] => Toplevel.ignored (#1 range)
-    | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
-    handle ERROR msg => Toplevel.malformed (#1 core_range) msg
+    | [] => Toplevel.ignored full_range
+    | _ => Toplevel.malformed core_range "Exactly one command expected")
+    handle ERROR msg => Toplevel.malformed core_range msg
   end;
 
 fun parse_text thy init pos text =
diff -r e700ede0038f -r 8a20737e4ebf src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Jan 08 14:29:58 2021 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Jan 08 14:40:04 2021 +0100
@@ -33,10 +33,11 @@
   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 position: Position.T -> transition -> transition
+  val positions: Position.T -> Position.range -> transition -> transition
   val markers: Input.source list -> transition -> transition
   val timing: Time.time -> transition -> transition
   val init_theory: (unit -> theory) -> transition -> transition
@@ -46,9 +47,9 @@
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
   val keep_proof: (state -> unit) -> transition -> transition
-  val ignored: Position.T -> transition
   val is_ignored: transition -> bool
-  val malformed: Position.T -> string -> transition
+  val ignored: Position.range -> transition
+  val malformed: Position.range -> string -> transition
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
@@ -335,24 +336,27 @@
 
 datatype transition = Transition of
  {name: string,               (*command name*)
-  pos: Position.T,            (*source position*)
+  pos: Position.T,            (*source position: reference point*)
+  body_range: Position.range, (*source position: main body*)
   markers: Input.source list, (*semantic document markers*)
   timing: Time.time,          (*prescient timing information*)
   trans: trans list};         (*primitive transitions (union)*)
 
-fun make_transition (name, pos, markers, timing, trans) =
-  Transition {name = name, pos = pos, markers = markers, timing = timing, trans = trans};
+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 map_transition f (Transition {name, pos, markers, timing, trans}) =
-  make_transition (f (name, pos, markers, timing, trans));
+fun map_transition f (Transition {name, pos, body_range, markers, timing, trans}) =
+  make_transition (f (name, pos, body_range, markers, timing, trans));
 
-val empty = make_transition ("", Position.none, [], Time.zeroTime, []);
+val empty = make_transition ("", Position.none, Position.no_range, [], 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 =
@@ -365,23 +369,23 @@
 
 (* modify transitions *)
 
-fun name name = map_transition (fn (_, pos, markers, timing, trans) =>
-  (name, pos, markers, timing, trans));
+fun name name = map_transition (fn (_, pos, body_range, 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 positions pos body_range = map_transition (fn (name, _, _, markers, 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 markers markers = map_transition (fn (name, pos, body_range, _, timing, trans) =>
+  (name, pos, body_range, markers, timing, trans));
 
-fun timing timing = map_transition (fn (name, pos, markers, _, 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 add_trans tr = map_transition (fn (name, pos, markers, timing, trans) =>
-  (name, pos, markers, timing, tr :: trans));
+fun add_trans tr = map_transition (fn (name, pos, body_range, markers, timing, trans) =>
+  (name, pos, body_range, markers, timing, tr :: trans));
 
-val reset_trans = map_transition (fn (name, pos, markers, timing, _) =>
-  (name, pos, markers, timing, []));
+val reset_trans = map_transition (fn (name, pos, body_range, markers, timing, _) =>
+  (name, pos, body_range, markers, timing, []));
 
 
 (* basic transitions *)
@@ -408,11 +412,13 @@
     else if is_skipped_proof st then ()
     else warning "No proof state");
 
-fun ignored pos = empty |> name "<ignored>" |> position pos |> keep (fn _ => ());
 fun is_ignored tr = name_of tr = "<ignored>";
 
-fun malformed pos msg =
-  empty |> name "<malformed>" |> position pos |> keep (fn _ => error msg);
+fun ignored range =
+  empty |> name "<ignored>" |> positions (#1 range) range |> keep (fn _ => ());
+
+fun malformed range msg =
+  empty |> name "<malformed>" |> positions (#1 range) range |> keep (fn _ => error msg);
 
 
 (* theory transitions *)
@@ -592,8 +598,9 @@
 
 (* runtime position *)
 
-fun exec_id id (tr as Transition {pos, ...}) =
-  position (Position.put_id (Document_ID.print id) pos) tr;
+fun exec_id id (tr as Transition {pos, body_range, ...}) =
+  let val put_id = Position.put_id (Document_ID.print id)
+  in positions (put_id pos) (apply2 put_id body_range) tr end;
 
 fun setmp_thread_position (Transition {pos, ...}) f x =
   Position.setmp_thread_data pos f x;
diff -r e700ede0038f -r 8a20737e4ebf src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Jan 08 14:29:58 2021 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Jan 08 14:40:04 2021 +0100
@@ -156,7 +156,7 @@
         Position.here_list verbatim);
   in
     if exists #1 token_reports
-    then Toplevel.malformed (#1 (Token.core_range_of span)) "Malformed command syntax"
+    then Toplevel.malformed (Token.core_range_of span) "Malformed command syntax"
     else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span)
   end;