src/Tools/VSCode/src/vscode_rendering.scala
changeset 64652 ad55f164ae0d
parent 64651 ea5620f7b0d8
child 64654 31b681e38c70
     1.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 22:49:53 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 22:52:07 2016 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  object VSCode_Rendering
     1.5  {
     1.6    private val hyperlink_elements =
     1.7 -    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
     1.8 +    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION)
     1.9  }
    1.10  
    1.11  class VSCode_Rendering(
    1.12 @@ -40,9 +40,6 @@
    1.13              Some(Line.Node_Range(resolve_file_url(name)) :: links)
    1.14  
    1.15  /* FIXME
    1.16 -          case (links, Text.Info(_, XML.Elem(Markup.Url(name), _))) =>
    1.17 -            Some(PIDE.editor.hyperlink_url(name) :: links)
    1.18 -
    1.19            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    1.20            if !props.exists(
    1.21              { case (Markup.KIND, Markup.ML_OPEN) => true