tuned signature;
authorwenzelm
Tue Jul 31 21:06:09 2018 +0200 (9 months ago)
changeset 68728c07f6fa02c59
parent 68705 5cbd9cda7626
child 68729 3a02b424d5fb
tuned signature;
src/Pure/PIDE/command.ML
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle.scala
     1.1 --- a/src/Pure/PIDE/command.ML	Sun Jul 29 13:18:10 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Tue Jul 31 21:06:09 2018 +0200
     1.3 @@ -136,11 +136,11 @@
     1.4    let
     1.5      val command_reports = Outer_Syntax.command_reports thy;
     1.6  
     1.7 -    val proper_range = Token.range_of (drop_suffix Token.is_improper span);
     1.8 +    val core_range = Token.range_of (drop_suffix Token.is_improper span);
     1.9      val pos =
    1.10        (case find_first Token.is_command span of
    1.11          SOME tok => Token.pos_of tok
    1.12 -      | NONE => #1 proper_range);
    1.13 +      | NONE => #1 core_range);
    1.14  
    1.15      val token_reports = map (reports_of_token keywords) span;
    1.16      val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span);
    1.17 @@ -150,8 +150,8 @@
    1.18        (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
    1.19          [tr] => Toplevel.modify_init init tr
    1.20        | [] => Toplevel.ignored (#1 (Token.range_of span))
    1.21 -      | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
    1.22 -      handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
    1.23 +      | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
    1.24 +      handle ERROR msg => Toplevel.malformed (#1 core_range) msg
    1.25    end;
    1.26  
    1.27  end;
     2.1 --- a/src/Pure/PIDE/command.scala	Sun Jul 29 13:18:10 2018 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Tue Jul 31 21:06:09 2018 +0200
     2.3 @@ -319,7 +319,7 @@
     2.4                case elem @ XML.Elem(markup, Nil) =>
     2.5                  state.
     2.6                    add_status(markup).
     2.7 -                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem))
     2.8 +                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
     2.9                case _ =>
    2.10                  Output.warning("Ignored status message: " + msg)
    2.11                  state
    2.12 @@ -355,7 +355,7 @@
    2.13  
    2.14                  case XML.Elem(Markup(name, atts), args)
    2.15                  if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
    2.16 -                  val range = command.proper_range
    2.17 +                  val range = command.core_range
    2.18                    val props = Position.purge(atts)
    2.19                    val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
    2.20                    state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem))
    2.21 @@ -603,7 +603,7 @@
    2.22    def length: Int = source.length
    2.23    def range: Text.Range = chunk.range
    2.24  
    2.25 -  val proper_range: Text.Range =
    2.26 +  val core_range: Text.Range =
    2.27      Text.Range(0,
    2.28        (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
    2.29  
     3.1 --- a/src/Pure/PIDE/document.scala	Sun Jul 29 13:18:10 2018 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Tue Jul 31 21:06:09 2018 +0200
     3.3 @@ -1024,7 +1024,7 @@
     3.4              blob_name <- cmd.blobs_names.iterator
     3.5              if pred(blob_name)
     3.6              start <- node.command_start(cmd)
     3.7 -          } yield convert(cmd.proper_range + start)).toList
     3.8 +          } yield convert(cmd.core_range + start)).toList
     3.9  
    3.10          def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
    3.11            if (other_node_name.is_theory) {
     4.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Jul 29 13:18:10 2018 +0200
     4.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Jul 31 21:06:09 2018 +0200
     4.3 @@ -81,7 +81,7 @@
     4.4          PIDE.editor.current_command(view, snapshot) match {
     4.5            case Some(command) =>
     4.6              snapshot.node.command_start(command) match {
     4.7 -              case Some(start) => List(snapshot.convert(command.proper_range + start))
     4.8 +              case Some(start) => List(snapshot.convert(command.core_range + start))
     4.9                case None => Nil
    4.10              }
    4.11            case None => Nil
     5.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sun Jul 29 13:18:10 2018 +0200
     5.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Jul 31 21:06:09 2018 +0200
     5.3 @@ -334,7 +334,7 @@
     5.4            node.command_start(command) match {
     5.5              case Some(start) =>
     5.6                JEdit_Lib.buffer_edit(buffer) {
     5.7 -                val range = command.proper_range + start
     5.8 +                val range = command.core_range + start
     5.9                  JEdit_Lib.buffer_edit(buffer) {
    5.10                    if (padding) {
    5.11                      text_area.moveCaretPosition(start + range.length)