full range for Position.Item;
authorwenzelm
Fri Dec 23 19:19:59 2016 +0100 (2016-12-23)
changeset 64667cdb0d559a24b
parent 64666 f6c6e25ef782
child 64668 39a6c88c059b
full range for Position.Item;
more hyperlinks for VSCode;
src/Pure/General/position.scala
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Pure/General/position.scala	Fri Dec 23 19:07:54 2016 +0100
     1.2 +++ b/src/Pure/General/position.scala	Fri Dec 23 19:19:59 2016 +0100
     1.3 @@ -66,40 +66,48 @@
     1.4  
     1.5    object Item_Id
     1.6    {
     1.7 -    def unapply(pos: T): Option[(Long, Symbol.Offset)] =
     1.8 +    def unapply(pos: T): Option[(Long, Symbol.Range)] =
     1.9        pos match {
    1.10 -        case Id(id) => Some((id, Offset.unapply(pos) getOrElse 0))
    1.11 +        case Id(id) =>
    1.12 +          val offset = Offset.unapply(pos) getOrElse 0
    1.13 +          val end_offset = End_Offset.unapply(pos) getOrElse (offset + 1)
    1.14 +          Some((id, Text.Range(offset, end_offset)))
    1.15          case _ => None
    1.16        }
    1.17    }
    1.18  
    1.19    object Item_Def_Id
    1.20    {
    1.21 -    def unapply(pos: T): Option[(Long, Symbol.Offset)] =
    1.22 +    def unapply(pos: T): Option[(Long, Symbol.Range)] =
    1.23        pos match {
    1.24 -        case Def_Id(id) => Some((id, Def_Offset.unapply(pos) getOrElse 0))
    1.25 +        case Def_Id(id) =>
    1.26 +          val offset = Def_Offset.unapply(pos) getOrElse 0
    1.27 +          val end_offset = Def_End_Offset.unapply(pos) getOrElse (offset + 1)
    1.28 +          Some((id, Text.Range(offset, end_offset)))
    1.29          case _ => None
    1.30        }
    1.31    }
    1.32  
    1.33    object Item_File
    1.34    {
    1.35 -    def unapply(pos: T): Option[(String, Int, Symbol.Offset)] =
    1.36 +    def unapply(pos: T): Option[(String, Int, Symbol.Range)] =
    1.37        pos match {
    1.38          case Line_File(line, name) =>
    1.39 -          val offset = Position.Offset.unapply(pos) getOrElse 0
    1.40 -          Some((name, line, offset))
    1.41 +          val offset = Offset.unapply(pos) getOrElse 0
    1.42 +          val end_offset = End_Offset.unapply(pos) getOrElse (offset + 1)
    1.43 +          Some((name, line, Text.Range(offset, end_offset)))
    1.44          case _ => None
    1.45        }
    1.46    }
    1.47  
    1.48    object Item_Def_File
    1.49    {
    1.50 -    def unapply(pos: T): Option[(String, Int, Symbol.Offset)] =
    1.51 +    def unapply(pos: T): Option[(String, Int, Symbol.Range)] =
    1.52        pos match {
    1.53          case Def_Line_File(line, name) =>
    1.54 -          val offset = Position.Def_Offset.unapply(pos) getOrElse 0
    1.55 -          Some((name, line, offset))
    1.56 +          val offset = Def_Offset.unapply(pos) getOrElse 0
    1.57 +          val end_offset = Def_End_Offset.unapply(pos) getOrElse (offset + 1)
    1.58 +          Some((name, line, Text.Range(offset, end_offset)))
    1.59          case _ => None
    1.60        }
    1.61    }
     2.1 --- a/src/Tools/VSCode/src/document_model.scala	Fri Dec 23 19:07:54 2016 +0100
     2.2 +++ b/src/Tools/VSCode/src/document_model.scala	Fri Dec 23 19:19:59 2016 +0100
     2.3 @@ -56,6 +56,6 @@
     2.4  
     2.5    def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
     2.6  
     2.7 -  def rendering(options: Options): VSCode_Rendering =
     2.8 -    new VSCode_Rendering(this, snapshot(), options, session.resources)
     2.9 +  def rendering(options: Options, text_length: Length): VSCode_Rendering =
    2.10 +    new VSCode_Rendering(this, snapshot(), options, text_length, session.resources)
    2.11  }
     3.1 --- a/src/Tools/VSCode/src/server.scala	Fri Dec 23 19:07:54 2016 +0100
     3.2 +++ b/src/Tools/VSCode/src/server.scala	Fri Dec 23 19:19:59 2016 +0100
     3.3 @@ -109,7 +109,7 @@
     3.4    def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     3.5      for {
     3.6        model <- state.value.models.get(node_pos.name)
     3.7 -      rendering = model.rendering(options)
     3.8 +      rendering = model.rendering(options, text_length)
     3.9        offset <- model.doc.offset(node_pos.pos, text_length)
    3.10      } yield (rendering, offset)
    3.11  
     4.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Dec 23 19:07:54 2016 +0100
     4.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Dec 23 19:19:59 2016 +0100
     4.3 @@ -20,6 +20,7 @@
     4.4      val model: Document_Model,
     4.5      snapshot: Document.Snapshot,
     4.6      options: Options,
     4.7 +    text_length: Length,
     4.8      resources: Resources)
     4.9    extends Rendering(snapshot, options, resources)
    4.10  {
    4.11 @@ -31,6 +32,51 @@
    4.12  
    4.13    /* hyperlinks */
    4.14  
    4.15 +  def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
    4.16 +    : Option[Line.Node_Range] =
    4.17 +  {
    4.18 +    for (name <- resources.source_file(source_name))
    4.19 +    yield {
    4.20 +      val opt_text =
    4.21 +        try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models
    4.22 +        catch { case ERROR(_) => None }
    4.23 +      Line.Node_Range(name,
    4.24 +        opt_text match {
    4.25 +          case Some(text) if range.start > 0 =>
    4.26 +            val chunk = Symbol.Text_Chunk(text)
    4.27 +            val doc = Line.Document(text)
    4.28 +            def position(offset: Symbol.Offset) = doc.position(chunk.decode(offset), text_length)
    4.29 +            Line.Range(position(range.start), position(range.stop))
    4.30 +          case _ =>
    4.31 +            Line.Range(Line.Position((line1 - 1) max 0))
    4.32 +        })
    4.33 +    }
    4.34 +  }
    4.35 +
    4.36 +  def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] =
    4.37 +  {
    4.38 +    if (snapshot.is_outdated) None
    4.39 +    else
    4.40 +      for {
    4.41 +        start <- snapshot.find_command_position(id, range.start)
    4.42 +        stop <- snapshot.find_command_position(id, range.stop)
    4.43 +      } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos))
    4.44 +  }
    4.45 +
    4.46 +  def hyperlink_position(pos: Position.T): Option[Line.Node_Range] =
    4.47 +    pos match {
    4.48 +      case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range)
    4.49 +      case Position.Item_Id(id, range) => hyperlink_command(id, range)
    4.50 +      case _ => None
    4.51 +    }
    4.52 +
    4.53 +  def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] =
    4.54 +    pos match {
    4.55 +      case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range)
    4.56 +      case Position.Item_Def_Id(id, range) => hyperlink_command(id, range)
    4.57 +      case _ => None
    4.58 +    }
    4.59 +
    4.60    def hyperlinks(range: Text.Range): List[Line.Node_Range] =
    4.61    {
    4.62      snapshot.cumulate[List[Line.Node_Range]](
    4.63 @@ -40,7 +86,11 @@
    4.64              val file = resources.append_file_url(snapshot.node_name.master_dir, name)
    4.65              Some(Line.Node_Range(file) :: links)
    4.66  
    4.67 -          // FIXME more cases
    4.68 +          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    4.69 +            hyperlink_def_position(props).map(_ :: links)
    4.70 +
    4.71 +          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    4.72 +            hyperlink_position(props).map(_ :: links)
    4.73  
    4.74            case _ => None
    4.75          }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
     5.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 19:07:54 2016 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 19:19:59 2016 +0100
     5.3 @@ -291,11 +291,11 @@
     5.4      text_offset: Text.Offset, pos: Position.T): Boolean =
     5.5    {
     5.6      pos match {
     5.7 -      case Position.Item_Id(id, offset) if offset > 0 =>
     5.8 +      case Position.Item_Id(id, range) if range.start > 0 =>
     5.9          snapshot.find_command(id) match {
    5.10            case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
    5.11              node.command_start(command) match {
    5.12 -              case Some(start) => text_offset == start + command.chunk.decode(offset)
    5.13 +              case Some(start) => text_offset == start + command.chunk.decode(range.start)
    5.14                case None => false
    5.15              }
    5.16            case _ => false
    5.17 @@ -307,20 +307,20 @@
    5.18    def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
    5.19        : Option[Hyperlink] =
    5.20      pos match {
    5.21 -      case Position.Item_File(name, line, offset) =>
    5.22 -        hyperlink_source_file(focus, name, line, offset)
    5.23 -      case Position.Item_Id(id, offset) =>
    5.24 -        hyperlink_command(focus, snapshot, id, offset)
    5.25 +      case Position.Item_File(name, line, range) =>
    5.26 +        hyperlink_source_file(focus, name, line, range.start)
    5.27 +      case Position.Item_Id(id, range) =>
    5.28 +        hyperlink_command(focus, snapshot, id, range.start)
    5.29        case _ => None
    5.30      }
    5.31  
    5.32    def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
    5.33        : Option[Hyperlink] =
    5.34      pos match {
    5.35 -      case Position.Item_Def_File(name, line, offset) =>
    5.36 -        hyperlink_source_file(focus, name, line, offset)
    5.37 -      case Position.Item_Def_Id(id, offset) =>
    5.38 -        hyperlink_command(focus, snapshot, id, offset)
    5.39 +      case Position.Item_Def_File(name, line, range) =>
    5.40 +        hyperlink_source_file(focus, name, line, range.start)
    5.41 +      case Position.Item_Def_Id(id, range) =>
    5.42 +        hyperlink_command(focus, snapshot, id, range.start)
    5.43        case _ => None
    5.44      }
    5.45  }