--- a/src/Pure/General/file.scala Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/General/file.scala Tue Jan 03 21:03:11 2017 +0100
@@ -33,7 +33,7 @@
if (Platform.is_windows) {
val Platform_Root = new Regex("(?i)" +
Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
- val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
+ val Drive = new Regex("""\\?([a-zA-Z]):\\*(.*)""")
platform_path.replace('/', '\\') match {
case Platform_Root(rest) => "/" + rest.replace('\\', '/')
@@ -48,6 +48,7 @@
def standard_path(file: JFile): String = standard_path(file.getPath)
def path(file: JFile): Path = Path.explode(standard_path(file))
+ def pwd(): Path = path(Path.current.file.toPath.toAbsolutePath.toFile)
def standard_url(name: String): String =
try {
--- a/src/Pure/General/json.scala Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/General/json.scala Tue Jan 03 21:03:11 2017 +0100
@@ -32,7 +32,19 @@
def string(s: String)
{
result += '"'
- result ++= scala.util.parsing.json.JSONFormat.quoteString(s)
+ result ++=
+ s.iterator.map {
+ case '"' => "\\\""
+ case '\\' => "\\\\"
+ case '\b' => "\\b"
+ case '\f' => "\\f"
+ case '\n' => "\\n"
+ case '\r' => "\\r"
+ case '\t' => "\\t"
+ case c =>
+ if (c <= '\u001f' || c >= '\u007f' && c <= '\u009f') "\\u%04x".format(c.toInt)
+ else c
+ }.mkString
result += '"'
}
--- a/src/Pure/General/url.scala Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/General/url.scala Tue Jan 03 21:03:11 2017 +0100
@@ -57,6 +57,19 @@
try { file(uri); true }
catch { case _: URISyntaxException | _: IllegalArgumentException => false }
+ def normalize_file(uri: String): String =
+ if (is_wellformed_file(uri)) {
+ val uri1 = new URI(uri).normalize.toASCIIString
+ if (uri1.startsWith("file://")) uri1
+ else {
+ Library.try_unprefix("file:/", uri1) match {
+ case Some(p) => "file:///" + p
+ case None => uri1
+ }
+ }
+ }
+ else uri
+
def platform_file(path: Path): String =
{
val path1 = path.expand
@@ -68,8 +81,6 @@
if (name.startsWith("file://")) name
else {
val s = name.replaceAll(" ", "%20")
- if (!Platform.is_windows) "file://" + s
- else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
- else "file:///" + s.replace('\\', '/')
+ "file://" + (if (Platform.is_windows) s.replace('\\', '/') else s)
}
}
--- a/src/Pure/PIDE/line.scala Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/PIDE/line.scala Tue Jan 03 21:03:11 2017 +0100
@@ -125,8 +125,7 @@
val c = pos.column
if (0 <= l && l < lines.length) {
val line_offset =
- if (l == 0) 0
- else (0 /: lines.iterator.take(l - 1)) { case (n, line) => n + text_length(line.text) + 1 }
+ (0 /: lines.iterator.take(l)) { case (n, line) => n + text_length(line.text) + 1 }
text_length.offset(lines(l).text, c).map(line_offset + _)
}
else None
--- a/src/Pure/PIDE/rendering.scala Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/PIDE/rendering.scala Tue Jan 03 21:03:11 2017 +0100
@@ -58,6 +58,8 @@
private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
+
+ val caret_focus_elements = Markup.Elements(Markup.ENTITY)
}
abstract class Rendering(
@@ -162,4 +164,53 @@
Some(Text.Info(r, all_tips))
}
}
+
+
+ /* caret focus */
+
+ private def entity_focus(range: Text.Range,
+ check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
+ {
+ val results =
+ snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
+ {
+ case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
+ props match {
+ case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
+ case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
+ case _ => None
+ }
+ case _ => None
+ })
+ (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
+ }
+
+ def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
+ {
+ val focus_defs = entity_focus(caret_range)
+ if (focus_defs.nonEmpty) focus_defs
+ else {
+ val visible_defs = entity_focus(visible_range)
+ entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
+ }
+ }
+
+ def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
+ {
+ val focus = caret_focus(caret_range, visible_range)
+ if (focus.nonEmpty) {
+ val results =
+ snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
+ {
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
+ props match {
+ case Markup.Entity.Def(i) if focus(i) => Some(true)
+ case Markup.Entity.Ref(i) if focus(i) => Some(true)
+ case _ => None
+ }
+ })
+ for (info <- results if info.info) yield info.range
+ }
+ else Nil
+ }
}
--- a/src/Pure/PIDE/resources.scala Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/PIDE/resources.scala Tue Jan 03 21:03:11 2017 +0100
@@ -48,10 +48,6 @@
if (Path.is_valid(raw_name)) append(dir, Path.explode(raw_name))
else raw_name
- def append_file_url(dir: String, raw_name: String): String =
- if (Path.is_valid(raw_name)) "file://" + append(dir, Path.explode(raw_name))
- else raw_name
-
/* source files of Isabelle/ML bootstrap */
--- a/src/Pure/Thy/thy_header.scala Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/Thy/thy_header.scala Tue Jan 03 21:03:11 2017 +0100
@@ -77,9 +77,13 @@
val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
+ private val Dir_Name = new Regex("""(.*?)[^/\\:]+""")
private val Base_Name = new Regex(""".*?([^/\\:]+)""")
private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
+ def dir_name(s: String): String =
+ s match { case Dir_Name(name) => name case _ => "" }
+
def base_name(s: String): String =
s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
--- a/src/Tools/VSCode/extension/isabelle-language.json Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/VSCode/extension/isabelle-language.json Tue Jan 03 21:03:11 2017 +0100
@@ -1,18 +1,48 @@
{
- "brackets": [
- ["(", ")"],
- ["[", "]"],
- ["{", "}"],
- ["«", "»"],
- ["‹", "›"],
- ["⟨", "⟩"],
- ["⌈", "⌉"],
- ["⌊", "⌋"],
- ["⦇", "⦈"],
- ["⟦", "⟧"],
- ["⦃", "⦄"]
- ],
- "comments": {
- "blockComment": [ "(*", "*)" ]
- }
+ "comments": {
+ "blockComment": ["(*", "*)"]
+ },
+ "brackets": [
+ ["(", ")"],
+ ["[", "]"],
+ ["{", "}"],
+ ["«", "»"],
+ ["‹", "›"],
+ ["⟨", "⟩"],
+ ["⌈", "⌉"],
+ ["⌊", "⌋"],
+ ["⦇", "⦈"],
+ ["⟦", "⟧"],
+ ["⦃", "⦄"]
+ ],
+ "autoClosingPairs": [
+ { "open": "(", "close": ")" },
+ { "open": "[", "close": "]" },
+ { "open": "{", "close": "}" },
+ { "open": "«", "close": "»" },
+ { "open": "‹", "close": "›" },
+ { "open": "⟨", "close": "⟩" },
+ { "open": "⌈", "close": "⌉" },
+ { "open": "⌊", "close": "⌋" },
+ { "open": "⦇", "close": "⦈" },
+ { "open": "⟦", "close": "⟧" },
+ { "open": "⦃", "close": "⦄" },
+ { "open": "`", "close": "`", "notIn": ["string"] },
+ { "open": "\"", "close": "\"", "notIn": ["string"] }
+ ],
+ "surroundingPairs": [
+ ["(", ")"],
+ ["[", "]"],
+ ["{", "}"],
+ ["«", "»"],
+ ["‹", "›"],
+ ["⟨", "⟩"],
+ ["⌈", "⌉"],
+ ["⌊", "⌋"],
+ ["⦇", "⦈"],
+ ["⟦", "⟧"],
+ ["⦃", "⦄"],
+ ["`", "`"],
+ ["\"", "\""]
+ ]
}
--- a/src/Tools/VSCode/extension/isabelle-ml-language.json Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/VSCode/extension/isabelle-ml-language.json Tue Jan 03 21:03:11 2017 +0100
@@ -1,18 +1,18 @@
{
+ "comments": {
+ "blockComment": [ "(*", "*)" ]
+ },
+ "brackets": [
+ ["(", ")"],
+ ["[", "]"],
+ ["{", "}"]
+ ],
"autoClosingPairs": [
{ "open": "{", "close": "}" },
{ "open": "[", "close": "]" },
{ "open": "(", "close": ")" },
{ "open": "\"", "close": "\"", "notIn": [ "string" ] }
],
- "brackets": [
- ["(", ")"],
- ["[", "]"],
- ["{", "}"]
- ],
- "comments": {
- "blockComment": [ "(*", "*)" ]
- },
"surroundingPairs": [
[ "{", "}" ],
[ "[", "]" ],
--- a/src/Tools/VSCode/src/protocol.scala Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/VSCode/src/protocol.scala Tue Jan 03 21:03:11 2017 +0100
@@ -138,7 +138,8 @@
Map(
"textDocumentSync" -> 1,
"hoverProvider" -> true,
- "definitionProvider" -> true)
+ "definitionProvider" -> true,
+ "documentHighlightProvider" -> true)
}
object Shutdown extends Request0("shutdown")
@@ -315,6 +316,31 @@
}
+ /* document highlights request */
+
+ object DocumentHighlight
+ {
+ def text(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(1))
+ def read(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(2))
+ def write(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(3))
+ }
+
+ sealed case class DocumentHighlight(range: Line.Range, kind: Option[Int] = None)
+ {
+ def json: JSON.T =
+ kind match {
+ case None => Map("range" -> Range(range))
+ case Some(k) => Map("range" -> Range(range), "kind" -> k)
+ }
+ }
+
+ object DocumentHighlights extends RequestTextDocumentPosition("textDocument/documentHighlight")
+ {
+ def reply(id: Id, result: List[DocumentHighlight]): JSON.T =
+ ResponseMessage(id, Some(result.map(_.json)))
+ }
+
+
/* diagnostics */
sealed case class Diagnostic(range: Line.Range, message: String,
@@ -329,10 +355,10 @@
object DiagnosticSeverity
{
- val Error = 0
- val Warning = 1
- val Information = 2
- val Hint = 3
+ val Error = 1
+ val Warning = 2
+ val Information = 3
+ val Hint = 4
}
object PublishDiagnostics
--- a/src/Tools/VSCode/src/server.scala Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/VSCode/src/server.scala Tue Jan 03 21:03:11 2017 +0100
@@ -303,6 +303,21 @@
}
+ /* document highlights */
+
+ def document_highlights(id: Protocol.Id, node_pos: Line.Node_Position)
+ {
+ val result =
+ (for ((rendering, offset) <- rendering_offset(node_pos))
+ yield {
+ val doc = rendering.model.doc
+ rendering.caret_focus_ranges(Text.Range(offset, offset + 1), doc.full_range)
+ .map(r => Protocol.DocumentHighlight.text(doc.range(r)))
+ }) getOrElse Nil
+ channel.write(Protocol.DocumentHighlights.reply(id, result))
+ }
+
+
/* main loop */
def start()
@@ -324,6 +339,7 @@
close_document(uri)
case Protocol.Hover(id, node_pos) => hover(id, node_pos)
case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
+ case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
case _ => log("### IGNORED")
}
}
--- a/src/Tools/VSCode/src/vscode_rendering.scala Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Tue Jan 03 21:03:11 2017 +0100
@@ -16,7 +16,7 @@
private val message_severity =
Map(
- Markup.WRITELN -> Protocol.DiagnosticSeverity.Hint,
+ Markup.WRITELN -> Protocol.DiagnosticSeverity.Information,
Markup.INFORMATION -> Protocol.DiagnosticSeverity.Information,
Markup.WARNING -> Protocol.DiagnosticSeverity.Warning,
Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
@@ -126,7 +126,7 @@
range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
{
case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
- val file = resources.append_file_url(snapshot.node_name.master_dir, name)
+ val file = resources.append_file(snapshot.node_name.master_dir, name)
Some(Line.Node_Range(file) :: links)
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
--- a/src/Tools/VSCode/src/vscode_resources.scala Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Jan 03 21:03:11 2017 +0100
@@ -43,16 +43,17 @@
val theory = Thy_Header.thy_name_bootstrap(uri).getOrElse("")
val master_dir =
if (!Url.is_wellformed_file(uri) || theory == "") ""
- else Url.file(uri).getCanonicalFile.getParent
+ else Thy_Header.dir_name(uri)
Document.Node.Name(uri, master_dir, theory)
}
- override def import_name(qualifier: String, master: Document.Node.Name, s: String)
- : Document.Node.Name =
+ override def append(dir: String, source_path: Path): String =
{
- val name = super.import_name(qualifier, master, s)
- if (name.node.startsWith("file://") || name.node.forall(c => c != '/' && c != '\\')) name
- else name.copy(node = "file://" + name.node)
+ val path = source_path.expand
+ if (path.is_absolute) Url.platform_file(path)
+ else if (dir == "") Url.platform_file(File.pwd() + path)
+ else if (path.is_current) dir
+ else Url.normalize_file(dir + "/" + path.implode)
}
override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
--- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Tue Jan 03 21:03:11 2017 +0100
@@ -127,8 +127,6 @@
private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
- private val caret_focus_elements = Markup.Elements(Markup.ENTITY)
-
private val highlight_elements =
Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
@@ -367,54 +365,8 @@
/* caret focus */
- def entity_focus(range: Text.Range,
- check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
- {
- val results =
- snapshot.cumulate[Set[Long]](range, Set.empty, JEdit_Rendering.caret_focus_elements, _ =>
- {
- case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
- props match {
- case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
- case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
- case _ => None
- }
- case _ => None
- })
- (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
- }
-
- def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
- {
- val focus_defs = entity_focus(caret_range)
- if (focus_defs.nonEmpty) focus_defs
- else {
- val visible_defs = entity_focus(visible_range)
- entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
- }
- }
-
- def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
- {
- val focus = caret_focus(caret_range, visible_range)
- if (focus.nonEmpty) {
- val results =
- snapshot.cumulate[Boolean](visible_range, false, JEdit_Rendering.caret_focus_elements, _ =>
- {
- case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
- props match {
- case Markup.Entity.Def(i) if focus(i) => Some(true)
- case Markup.Entity.Ref(i) if focus(i) => Some(true)
- case _ => None
- }
- })
- for (info <- results if info.info) yield info.range
- }
- else Nil
- }
-
def entity_ref(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
- snapshot.select(range, JEdit_Rendering.caret_focus_elements, _ =>
+ snapshot.select(range, Rendering.caret_focus_elements, _ =>
{
case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _)) if focus(i) =>
Some(entity_ref_color)