--- a/src/Pure/General/file.scala Wed Jan 04 16:33:58 2017 +0000
+++ b/src/Pure/General/file.scala Wed Jan 04 21:29:19 2017 +0100
@@ -13,7 +13,7 @@
import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath,
Files, SimpleFileVisitor, FileVisitResult}
import java.nio.file.attribute.BasicFileAttributes
-import java.net.{URL, URLDecoder, MalformedURLException}
+import java.net.{URL, MalformedURLException}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
import java.util.regex.Pattern
@@ -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('\\', '/')
@@ -53,8 +53,8 @@
def standard_url(name: String): String =
try {
val url = new URL(name)
- if (url.getProtocol == "file")
- standard_path(URLDecoder.decode(url.getPath, UTF8.charset_name))
+ if (url.getProtocol == "file" && Url.is_wellformed_file(name))
+ standard_path(Url.parse_file(name))
else name
}
catch { case _: MalformedURLException => standard_path(name) }
--- a/src/Pure/General/url.ML Wed Jan 04 16:33:58 2017 +0000
+++ b/src/Pure/General/url.ML Wed Jan 04 21:29:19 2017 +0100
@@ -8,7 +8,6 @@
sig
datatype T =
File of Path.T |
- RemoteFile of string * Path.T |
Http of string * Path.T |
Ftp of string * Path.T
val append: T -> T -> T
@@ -25,17 +24,15 @@
datatype T =
File of Path.T |
- RemoteFile of string * Path.T |
Http of string * Path.T |
Ftp of string * Path.T;
(* append *)
-fun append (File p) (File p') = File (Path.append p p')
- | append (RemoteFile (h, p)) (File p') = RemoteFile (h, Path.append p p')
- | append (Http (h, p)) (File p') = Http (h, Path.append p p')
- | append (Ftp (h, p)) (File p') = Ftp (h, Path.append p p')
+fun append (File p) (File p') = File (Path.append p p')
+ | append (Http (h, p)) (File p') = Http (h, Path.append p p')
+ | append (Ftp (h, p)) (File p') = Ftp (h, Path.append p p')
| append _ url = url;
@@ -44,7 +41,6 @@
fun implode_path p = if Path.is_current p then "" else Path.implode p;
fun implode_url (File p) = implode_path p
- | implode_url (RemoteFile (h, p)) = "file://" ^ h ^ implode_path p
| implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
| implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
@@ -65,7 +61,8 @@
Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
Scan.this_string "file:///" |-- scan_path_root >> File ||
Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
- Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
+ Scan.this_string "file://" |-- scan_host -- scan_path
+ >> (fn (h, p) => File (Path.append (Path.named_root h) p)) ||
Scan.this_string "file:/" |-- scan_path_root >> File ||
Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
--- a/src/Pure/General/url.scala Wed Jan 04 16:33:58 2017 +0000
+++ b/src/Pure/General/url.scala Wed Jan 04 21:29:19 2017 +0100
@@ -8,6 +8,7 @@
import java.io.{File => JFile}
+import java.nio.file.Paths
import java.net.{URI, URISyntaxException}
import java.net.{URL, MalformedURLException}
import java.util.zip.GZIPInputStream
@@ -51,36 +52,15 @@
/* file URIs */
- def file(uri: String): JFile = new JFile(new URI(uri))
+ def print_file(file: JFile): String = file.toPath.toAbsolutePath.toUri.normalize.toString
+ def print_file_name(name: String): String = print_file(new JFile(name))
+
+ def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile
def is_wellformed_file(uri: String): Boolean =
- try { file(uri); true }
+ try { parse_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
- require(path1.is_absolute)
- platform_file(File.platform_path(path1))
- }
-
- def platform_file(name: String): String =
- if (name.startsWith("file://")) name
- else {
- val s = name.replaceAll(" ", "%20")
- "file://" + (if (Platform.is_windows) s.replace('\\', '/') else s)
- }
+ def canonical_file(uri: String): JFile = parse_file(uri).getCanonicalFile
+ def canonical_file_name(uri: String): String = canonical_file(uri).getPath
}
--- a/src/Pure/Thy/thy_header.scala Wed Jan 04 16:33:58 2017 +0000
+++ b/src/Pure/Thy/thy_header.scala Wed Jan 04 21:29:19 2017 +0100
@@ -77,13 +77,9 @@
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/package.json Wed Jan 04 16:33:58 2017 +0000
+++ b/src/Tools/VSCode/extension/package.json Wed Jan 04 21:29:19 2017 +0100
@@ -32,7 +32,7 @@
{
"id": "isabelle-ml",
"aliases": ["Isabelle/ML"],
- "extensions": [".ML"],
+ "extensions": [".ML", ".sml", ".sig"],
"configuration": "./isabelle-ml-language.json"
}
--- a/src/Tools/VSCode/src/channel.scala Wed Jan 04 16:33:58 2017 +0000
+++ b/src/Tools/VSCode/src/channel.scala Wed Jan 04 21:29:19 2017 +0100
@@ -9,7 +9,7 @@
import isabelle._
-import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream}
+import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream, File => JFile}
import scala.collection.mutable
@@ -111,6 +111,6 @@
/* diagnostics */
- def diagnostics(uri: String, diagnostics: List[Protocol.Diagnostic]): Unit =
- write(Protocol.PublishDiagnostics(uri, diagnostics))
+ def diagnostics(file: JFile, diagnostics: List[Protocol.Diagnostic]): Unit =
+ write(Protocol.PublishDiagnostics(file, diagnostics))
}
--- a/src/Tools/VSCode/src/document_model.scala Wed Jan 04 16:33:58 2017 +0000
+++ b/src/Tools/VSCode/src/document_model.scala Wed Jan 04 21:29:19 2017 +0100
@@ -16,10 +16,9 @@
object Document_Model
{
- def init(session: Session, uri: String): Document_Model =
+ def init(session: Session, node_name: Document.Node.Name): Document_Model =
{
val resources = session.resources.asInstanceOf[VSCode_Resources]
- val node_name = resources.node_name(uri)
val doc = Line.Document("", resources.text_length)
Document_Model(session, node_name, doc)
}
@@ -39,22 +38,13 @@
override def toString: String = node_name.toString
- def uri: String = node_name.node
def is_theory: Boolean = node_name.is_theory
/* external file */
- val file: JFile = Url.file(uri).getCanonicalFile
-
def external(b: Boolean): Document_Model = copy(external_file = b)
- def register(watcher: File_Watcher)
- {
- val dir = file.getParentFile
- if (dir != null && dir.isDirectory) watcher.register(dir)
- }
-
/* header */
@@ -94,13 +84,6 @@
}
}
- def update_file: Option[Document_Model] =
- if (external_file) {
- try { update_text(File.read(file)) }
- catch { case ERROR(_) => None }
- }
- else None
-
def flush_edits: Option[(List[Document.Edit_Text], Document_Model)] =
{
val perspective = node_perspective
--- a/src/Tools/VSCode/src/protocol.scala Wed Jan 04 16:33:58 2017 +0000
+++ b/src/Tools/VSCode/src/protocol.scala Wed Jan 04 21:29:19 2017 +0100
@@ -11,6 +11,9 @@
import isabelle._
+import java.io.{File => JFile}
+
+
object Protocol
{
/* abstract message */
@@ -180,14 +183,14 @@
object Location
{
def apply(loc: Line.Node_Range): JSON.T =
- Map("uri" -> loc.name, "range" -> Range(loc.range))
+ Map("uri" -> Url.print_file_name(loc.name), "range" -> Range(loc.range))
def unapply(json: JSON.T): Option[Line.Node_Range] =
for {
uri <- JSON.string(json, "uri")
range_json <- JSON.value(json, "range")
range <- Range.unapply(range_json)
- } yield Line.Node_Range(uri, range)
+ } yield Line.Node_Range(Url.canonical_file_name(uri), range)
}
object TextDocumentPosition
@@ -198,7 +201,7 @@
uri <- JSON.string(doc, "uri")
pos_json <- JSON.value(json, "position")
pos <- Position.unapply(pos_json)
- } yield Line.Node_Position(uri, pos)
+ } yield Line.Node_Position(Url.canonical_file_name(uri), pos)
}
@@ -224,7 +227,7 @@
object DidOpenTextDocument
{
- def unapply(json: JSON.T): Option[(String, String, Long, String)] =
+ def unapply(json: JSON.T): Option[(JFile, String, Long, String)] =
json match {
case Notification("textDocument/didOpen", Some(params)) =>
for {
@@ -233,7 +236,7 @@
lang <- JSON.string(doc, "languageId")
version <- JSON.long(doc, "version")
text <- JSON.string(doc, "text")
- } yield (uri, lang, version, text)
+ } yield (Url.canonical_file(uri), lang, version, text)
case _ => None
}
}
@@ -259,7 +262,7 @@
object DidChangeTextDocument
{
- def unapply(json: JSON.T): Option[(String, Long, List[TextDocumentContentChange])] =
+ def unapply(json: JSON.T): Option[(JFile, Long, List[TextDocumentContentChange])] =
json match {
case Notification("textDocument/didChange", Some(params)) =>
for {
@@ -267,20 +270,20 @@
uri <- JSON.string(doc, "uri")
version <- JSON.long(doc, "version")
changes <- JSON.array(params, "contentChanges", TextDocumentContentChange.unapply _)
- } yield (uri, version, changes)
+ } yield (Url.canonical_file(uri), version, changes)
case _ => None
}
}
class TextDocumentNotification(name: String)
{
- def unapply(json: JSON.T): Option[String] =
+ def unapply(json: JSON.T): Option[JFile] =
json match {
case Notification(method, Some(params)) if method == name =>
for {
doc <- JSON.value(params, "textDocument")
uri <- JSON.string(doc, "uri")
- } yield uri
+ } yield Url.canonical_file(uri)
case _ => None
}
}
@@ -363,8 +366,8 @@
object PublishDiagnostics
{
- def apply(uri: String, diagnostics: List[Diagnostic]): JSON.T =
+ def apply(file: JFile, diagnostics: List[Diagnostic]): JSON.T =
Notification("textDocument/publishDiagnostics",
- Map("uri" -> uri, "diagnostics" -> diagnostics.map(_.json)))
+ Map("uri" -> Url.print_file(file), "diagnostics" -> diagnostics.map(_.json)))
}
}
--- a/src/Tools/VSCode/src/server.scala Wed Jan 04 16:33:58 2017 +0000
+++ b/src/Tools/VSCode/src/server.scala Wed Jan 04 21:29:19 2017 +0100
@@ -102,7 +102,7 @@
def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
for {
- model <- resources.get_model(node_pos.name)
+ model <- resources.get_model(new JFile(node_pos.name))
rendering = model.rendering()
offset <- model.doc.offset(node_pos.pos)
} yield (rendering, offset)
@@ -124,18 +124,19 @@
private def sync_documents(changed: Set[JFile]): Unit =
if (resources.sync_models(changed)) delay_input.invoke()
- private def update_document(uri: String, text: String)
+ private def update_document(file: JFile, text: String)
{
- resources.update_model(session, uri, text)
+ resources.update_model(session, file, text)
delay_input.invoke()
}
- private def close_document(uri: String)
+ private def close_document(file: JFile)
{
- resources.close_model(uri) match {
+ resources.close_model(file) match {
case Some(model) =>
- model.register(watcher)
- sync_documents(Set(model.file))
+ val dir = file.getParentFile
+ if (dir != null && dir.isDirectory) watcher.register(dir)
+ sync_documents(Set(file))
case None =>
}
}
@@ -153,7 +154,7 @@
private val prover_output =
Session.Consumer[Session.Commands_Changed](getClass.getName) {
case changed if changed.nodes.nonEmpty =>
- resources.update_output(changed.nodes.toList.map(_.node))
+ resources.update_output(changed.nodes.toList.map(resources.node_file(_)))
delay_output.invoke()
case _ =>
}
--- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Jan 04 16:33:58 2017 +0000
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Wed Jan 04 21:29:19 2017 +0100
@@ -10,6 +10,9 @@
import isabelle._
+import java.io.{File => JFile}
+
+
object VSCode_Rendering
{
/* diagnostic messages */
@@ -79,13 +82,15 @@
def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
: Option[Line.Node_Range] =
{
- for (name <- resources.source_file(source_name))
+ for {
+ platform_path <- resources.source_file(source_name)
+ file <-
+ (try { Some(new JFile(platform_path).getCanonicalFile) }
+ catch { case ERROR(_) => None })
+ }
yield {
- val opt_text =
- try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models
- catch { case ERROR(_) => None }
- Line.Node_Range(Url.platform_file(name),
- opt_text match {
+ Line.Node_Range(file.getPath,
+ resources.get_file_content(file) match {
case Some(text) if range.start > 0 =>
val chunk = Symbol.Text_Chunk(text)
val doc = Line.Document(text, resources.text_length)
--- a/src/Tools/VSCode/src/vscode_resources.scala Wed Jan 04 16:33:58 2017 +0000
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Jan 04 21:29:19 2017 +0100
@@ -19,9 +19,9 @@
/* internal state */
sealed case class State(
- models: Map[String, Document_Model] = Map.empty,
- pending_input: Set[String] = Set.empty,
- pending_output: Set[String] = Set.empty)
+ models: Map[JFile, Document_Model] = Map.empty,
+ pending_input: Set[JFile] = Set.empty,
+ pending_output: Set[JFile] = Set.empty)
}
class VSCode_Resources(
@@ -38,64 +38,65 @@
/* document node name */
- def node_name(uri: String): Document.Node.Name =
+ def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
+
+ def node_name(file: JFile): Document.Node.Name =
{
- val theory = Thy_Header.thy_name_bootstrap(uri).getOrElse("")
- val master_dir =
- if (!Url.is_wellformed_file(uri) || theory == "") ""
- else Thy_Header.dir_name(uri)
- Document.Node.Name(uri, master_dir, theory)
+ val node = file.getPath
+ val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
+ val master_dir = if (theory == "") "" else file.getParent
+ Document.Node.Name(node, master_dir, theory)
}
override def append(dir: String, source_path: Path): String =
{
val path = source_path.expand
- if (path.is_absolute) Url.platform_file(path)
- else if (dir == "") Url.platform_file(File.pwd() + path)
+ if (dir == "" || path.is_absolute) File.platform_path(path)
else if (path.is_current) dir
- else Url.normalize_file(dir + "/" + path.implode)
+ else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
+ dir + JFile.separator + File.platform_path(path)
+ else if (path.is_basic) dir + File.platform_path(path)
+ else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
}
override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
{
- val uri = name.node
- get_model(uri) match {
+ val file = node_file(name)
+ get_model(file) match {
case Some(model) =>
- val reader = new CharSequenceReader(model.doc.make_text)
- f(reader)
-
- case None =>
- val file = Url.file(uri)
- if (!file.isFile) error("No such file: " + quote(file.toString))
-
+ f(new CharSequenceReader(model.doc.make_text))
+ case None if file.isFile =>
val reader = Scan.byte_reader(file)
try { f(reader) } finally { reader.close }
+ case None =>
+ error("No such file: " + quote(file.toString))
}
}
/* document models */
- def get_model(uri: String): Option[Document_Model] = state.value.models.get(uri)
+ def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
+ def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
- def update_model(session: Session, uri: String, text: String)
+ def update_model(session: Session, file: JFile, text: String)
{
state.change(st =>
{
- val model = st.models.getOrElse(uri, Document_Model.init(session, uri))
+ val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file)))
val model1 = (model.update_text(text) getOrElse model).external(false)
st.copy(
- models = st.models + (uri -> model1),
- pending_input = st.pending_input + uri)
+ models = st.models + (file -> model1),
+ pending_input = st.pending_input + file)
})
}
- def close_model(uri: String): Option[Document_Model] =
+ def close_model(file: JFile): Option[Document_Model] =
state.change_result(st =>
- st.models.get(uri) match {
+ st.models.get(file) match {
case None => (None, st)
case Some(model) =>
- (Some(model), st.copy(models = st.models + (uri -> model.external(true))))
+ (Some(model), st.copy(models = st.models + (file -> model.external(true))))
})
def sync_models(changed_files: Set[JFile]): Boolean =
@@ -103,10 +104,11 @@
{
val changed_models =
(for {
- (uri, model) <- st.models.iterator
- if changed_files(model.file)
- model1 <- model.update_file
- } yield (uri, model1)).toList
+ (file, model) <- st.models.iterator
+ if changed_files(file) && model.external_file
+ text <- try_read(file)
+ model1 <- model.update_text(text)
+ } yield (file, model1)).toList
if (changed_models.isEmpty) (false, st)
else (true,
st.copy(
@@ -115,6 +117,19 @@
})
+ /* file content */
+
+ def try_read(file: JFile): Option[String] =
+ try { Some(File.read(file)) }
+ catch { case ERROR(_) => None }
+
+ def get_file_content(file: JFile): Option[String] =
+ get_model(file) match {
+ case Some(model) => Some(model.doc.make_text)
+ case None => try_read(file)
+ }
+
+
/* resolve dependencies */
val thy_info = new Thy_Info(this)
@@ -130,16 +145,14 @@
val loaded_models =
(for {
dep <- thy_info.dependencies("", thys).deps.iterator
- uri = dep.name.node
- if !st.models.isDefinedAt(uri)
- text <-
- try { Some(File.read(Url.file(uri))) }
- catch { case ERROR(_) => None }
+ file = node_file(dep.name)
+ if !st.models.isDefinedAt(file)
+ text <- try_read(file)
}
yield {
- val model = Document_Model.init(session, uri)
+ val model = Document_Model.init(session, node_name(file))
val model1 = (model.update_text(text) getOrElse model).external(true)
- (uri, model1)
+ (file, model1)
}).toList
if (loaded_models.isEmpty) (false, st)
@@ -160,14 +173,14 @@
{
val changed_models =
(for {
- uri <- st.pending_input.iterator
- model <- st.models.get(uri)
- res <- model.flush_edits
- } yield res).toList
+ file <- st.pending_input.iterator
+ model <- st.models.get(file)
+ (edits, model1) <- model.flush_edits
+ } yield (edits, (file, model1))).toList
session.update(Document.Blobs.empty, changed_models.flatMap(_._1))
st.copy(
- models = (st.models /: changed_models) { case (ms, (_, m)) => ms + (m.uri -> m) },
+ models = (st.models /: changed_models.iterator.map(_._2))(_ + _),
pending_input = Set.empty)
})
}
@@ -175,7 +188,7 @@
/* pending output */
- def update_output(changed_nodes: List[String]): Unit =
+ def update_output(changed_nodes: List[JFile]): Unit =
state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
def flush_output(channel: Channel)
@@ -184,16 +197,16 @@
{
val changed_iterator =
for {
- uri <- st.pending_output.iterator
- model <- st.models.get(uri)
+ file <- st.pending_output.iterator
+ model <- st.models.get(file)
rendering = model.rendering()
(diagnostics, model1) <- model.publish_diagnostics(rendering)
} yield {
- channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
- model1
+ channel.diagnostics(file, rendering.diagnostics_output(diagnostics))
+ (file, model1)
}
st.copy(
- models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
+ models = (st.models /: changed_iterator)(_ + _),
pending_output = Set.empty)
}
)