# HG changeset patch
# User wenzelm
# Date 1533063969 -7200
# Node ID c07f6fa02c5901765c6c5f06b2d1496be64f0b5e
# Parent  5cbd9cda76262996c60d70e9224687f47b943b72
tuned signature;

diff -r 5cbd9cda7626 -r c07f6fa02c59 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Jul 31 21:06:09 2018 +0200
@@ -136,11 +136,11 @@
   let
     val command_reports = Outer_Syntax.command_reports thy;
 
-    val proper_range = Token.range_of (drop_suffix Token.is_improper span);
+    val core_range = Token.range_of (drop_suffix Token.is_improper span);
     val pos =
       (case find_first Token.is_command span of
         SOME tok => Token.pos_of tok
-      | NONE => #1 proper_range);
+      | NONE => #1 core_range);
 
     val token_reports = map (reports_of_token keywords) span;
     val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span);
@@ -150,8 +150,8 @@
       (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
         [tr] => Toplevel.modify_init init tr
       | [] => Toplevel.ignored (#1 (Token.range_of span))
-      | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
-      handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
+      | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
+      handle ERROR msg => Toplevel.malformed (#1 core_range) msg
   end;
 
 end;
diff -r 5cbd9cda7626 -r c07f6fa02c59 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Jul 31 21:06:09 2018 +0200
@@ -319,7 +319,7 @@
               case elem @ XML.Elem(markup, Nil) =>
                 state.
                   add_status(markup).
-                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem))
+                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
               case _ =>
                 Output.warning("Ignored status message: " + msg)
                 state
@@ -355,7 +355,7 @@
 
                 case XML.Elem(Markup(name, atts), args)
                 if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
-                  val range = command.proper_range
+                  val range = command.core_range
                   val props = Position.purge(atts)
                   val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
                   state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem))
@@ -603,7 +603,7 @@
   def length: Int = source.length
   def range: Text.Range = chunk.range
 
-  val proper_range: Text.Range =
+  val core_range: Text.Range =
     Text.Range(0,
       (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
 
diff -r 5cbd9cda7626 -r c07f6fa02c59 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Jul 31 21:06:09 2018 +0200
@@ -1024,7 +1024,7 @@
             blob_name <- cmd.blobs_names.iterator
             if pred(blob_name)
             start <- node.command_start(cmd)
-          } yield convert(cmd.proper_range + start)).toList
+          } yield convert(cmd.core_range + start)).toList
 
         def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
           if (other_node_name.is_theory) {
diff -r 5cbd9cda7626 -r c07f6fa02c59 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Jul 31 21:06:09 2018 +0200
@@ -81,7 +81,7 @@
         PIDE.editor.current_command(view, snapshot) match {
           case Some(command) =>
             snapshot.node.command_start(command) match {
-              case Some(start) => List(snapshot.convert(command.proper_range + start))
+              case Some(start) => List(snapshot.convert(command.core_range + start))
               case None => Nil
             }
           case None => Nil
diff -r 5cbd9cda7626 -r c07f6fa02c59 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Jul 31 21:06:09 2018 +0200
@@ -334,7 +334,7 @@
           node.command_start(command) match {
             case Some(start) =>
               JEdit_Lib.buffer_edit(buffer) {
-                val range = command.proper_range + start
+                val range = command.core_range + start
                 JEdit_Lib.buffer_edit(buffer) {
                   if (padding) {
                     text_area.moveCaretPosition(start + range.length)