# HG changeset patch # User wenzelm # Date 1482517199 -3600 # Node ID cdb0d559a24b7a5415c96eb21a9c39e2b9cb4520 # Parent f6c6e25ef782876e5cab3dc00c674535b9f9aa31 full range for Position.Item; more hyperlinks for VSCode; diff -r f6c6e25ef782 -r cdb0d559a24b src/Pure/General/position.scala --- a/src/Pure/General/position.scala Fri Dec 23 19:07:54 2016 +0100 +++ b/src/Pure/General/position.scala Fri Dec 23 19:19:59 2016 +0100 @@ -66,40 +66,48 @@ object Item_Id { - def unapply(pos: T): Option[(Long, Symbol.Offset)] = + def unapply(pos: T): Option[(Long, Symbol.Range)] = pos match { - case Id(id) => Some((id, Offset.unapply(pos) getOrElse 0)) + case Id(id) => + val offset = Offset.unapply(pos) getOrElse 0 + val end_offset = End_Offset.unapply(pos) getOrElse (offset + 1) + Some((id, Text.Range(offset, end_offset))) case _ => None } } object Item_Def_Id { - def unapply(pos: T): Option[(Long, Symbol.Offset)] = + def unapply(pos: T): Option[(Long, Symbol.Range)] = pos match { - case Def_Id(id) => Some((id, Def_Offset.unapply(pos) getOrElse 0)) + case Def_Id(id) => + val offset = Def_Offset.unapply(pos) getOrElse 0 + val end_offset = Def_End_Offset.unapply(pos) getOrElse (offset + 1) + Some((id, Text.Range(offset, end_offset))) case _ => None } } object Item_File { - def unapply(pos: T): Option[(String, Int, Symbol.Offset)] = + def unapply(pos: T): Option[(String, Int, Symbol.Range)] = pos match { case Line_File(line, name) => - val offset = Position.Offset.unapply(pos) getOrElse 0 - Some((name, line, offset)) + val offset = Offset.unapply(pos) getOrElse 0 + val end_offset = End_Offset.unapply(pos) getOrElse (offset + 1) + Some((name, line, Text.Range(offset, end_offset))) case _ => None } } object Item_Def_File { - def unapply(pos: T): Option[(String, Int, Symbol.Offset)] = + def unapply(pos: T): Option[(String, Int, Symbol.Range)] = pos match { case Def_Line_File(line, name) => - val offset = Position.Def_Offset.unapply(pos) getOrElse 0 - Some((name, line, offset)) + val offset = Def_Offset.unapply(pos) getOrElse 0 + val end_offset = Def_End_Offset.unapply(pos) getOrElse (offset + 1) + Some((name, line, Text.Range(offset, end_offset))) case _ => None } } diff -r f6c6e25ef782 -r cdb0d559a24b src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Fri Dec 23 19:07:54 2016 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Fri Dec 23 19:19:59 2016 +0100 @@ -56,6 +56,6 @@ def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits) - def rendering(options: Options): VSCode_Rendering = - new VSCode_Rendering(this, snapshot(), options, session.resources) + def rendering(options: Options, text_length: Length): VSCode_Rendering = + new VSCode_Rendering(this, snapshot(), options, text_length, session.resources) } diff -r f6c6e25ef782 -r cdb0d559a24b src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Fri Dec 23 19:07:54 2016 +0100 +++ b/src/Tools/VSCode/src/server.scala Fri Dec 23 19:19:59 2016 +0100 @@ -109,7 +109,7 @@ def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] = for { model <- state.value.models.get(node_pos.name) - rendering = model.rendering(options) + rendering = model.rendering(options, text_length) offset <- model.doc.offset(node_pos.pos, text_length) } yield (rendering, offset) diff -r f6c6e25ef782 -r cdb0d559a24b src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Fri Dec 23 19:07:54 2016 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Fri Dec 23 19:19:59 2016 +0100 @@ -20,6 +20,7 @@ val model: Document_Model, snapshot: Document.Snapshot, options: Options, + text_length: Length, resources: Resources) extends Rendering(snapshot, options, resources) { @@ -31,6 +32,51 @@ /* hyperlinks */ + def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range) + : Option[Line.Node_Range] = + { + for (name <- resources.source_file(source_name)) + yield { + val opt_text = + try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models + catch { case ERROR(_) => None } + Line.Node_Range(name, + opt_text match { + case Some(text) if range.start > 0 => + val chunk = Symbol.Text_Chunk(text) + val doc = Line.Document(text) + def position(offset: Symbol.Offset) = doc.position(chunk.decode(offset), text_length) + Line.Range(position(range.start), position(range.stop)) + case _ => + Line.Range(Line.Position((line1 - 1) max 0)) + }) + } + } + + def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] = + { + if (snapshot.is_outdated) None + else + for { + start <- snapshot.find_command_position(id, range.start) + stop <- snapshot.find_command_position(id, range.stop) + } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos)) + } + + def hyperlink_position(pos: Position.T): Option[Line.Node_Range] = + pos match { + case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range) + case Position.Item_Id(id, range) => hyperlink_command(id, range) + case _ => None + } + + def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] = + pos match { + case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range) + case Position.Item_Def_Id(id, range) => hyperlink_command(id, range) + case _ => None + } + def hyperlinks(range: Text.Range): List[Line.Node_Range] = { snapshot.cumulate[List[Line.Node_Range]]( @@ -40,7 +86,11 @@ val file = resources.append_file_url(snapshot.node_name.master_dir, name) Some(Line.Node_Range(file) :: links) - // FIXME more cases + case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => + hyperlink_def_position(props).map(_ :: links) + + case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => + hyperlink_position(props).map(_ :: links) case _ => None }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil } diff -r f6c6e25ef782 -r cdb0d559a24b src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Fri Dec 23 19:07:54 2016 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Fri Dec 23 19:19:59 2016 +0100 @@ -291,11 +291,11 @@ text_offset: Text.Offset, pos: Position.T): Boolean = { pos match { - case Position.Item_Id(id, offset) if offset > 0 => + case Position.Item_Id(id, range) if range.start > 0 => snapshot.find_command(id) match { case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node => node.command_start(command) match { - case Some(start) => text_offset == start + command.chunk.decode(offset) + case Some(start) => text_offset == start + command.chunk.decode(range.start) case None => false } case _ => false @@ -307,20 +307,20 @@ def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T) : Option[Hyperlink] = pos match { - case Position.Item_File(name, line, offset) => - hyperlink_source_file(focus, name, line, offset) - case Position.Item_Id(id, offset) => - hyperlink_command(focus, snapshot, id, offset) + case Position.Item_File(name, line, range) => + hyperlink_source_file(focus, name, line, range.start) + case Position.Item_Id(id, range) => + hyperlink_command(focus, snapshot, id, range.start) case _ => None } def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T) : Option[Hyperlink] = pos match { - case Position.Item_Def_File(name, line, offset) => - hyperlink_source_file(focus, name, line, offset) - case Position.Item_Def_Id(id, offset) => - hyperlink_command(focus, snapshot, id, offset) + case Position.Item_Def_File(name, line, range) => + hyperlink_source_file(focus, name, line, range.start) + case Position.Item_Def_Id(id, range) => + hyperlink_command(focus, snapshot, id, range.start) case _ => None } }