# HG changeset patch # User wenzelm # Date 1483561759 -3600 # Node ID 31b5a28cadbc054a51244af93d251ba973cd8e63 # Parent 8cac34b3dcd007ed485fb5885a223ae5101477cb# Parent 99e8f7d4936f2ec30d9ff562162798920e21df82 merged diff -r 8cac34b3dcd0 -r 31b5a28cadbc src/Pure/General/file.scala --- 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) } diff -r 8cac34b3dcd0 -r 31b5a28cadbc src/Pure/General/url.ML --- 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; diff -r 8cac34b3dcd0 -r 31b5a28cadbc src/Pure/General/url.scala --- 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 } diff -r 8cac34b3dcd0 -r 31b5a28cadbc src/Pure/Thy/thy_header.scala --- 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)) } diff -r 8cac34b3dcd0 -r 31b5a28cadbc src/Tools/VSCode/extension/package.json --- 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" } diff -r 8cac34b3dcd0 -r 31b5a28cadbc src/Tools/VSCode/src/channel.scala --- 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)) } diff -r 8cac34b3dcd0 -r 31b5a28cadbc src/Tools/VSCode/src/document_model.scala --- 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 diff -r 8cac34b3dcd0 -r 31b5a28cadbc src/Tools/VSCode/src/protocol.scala --- 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))) } } diff -r 8cac34b3dcd0 -r 31b5a28cadbc src/Tools/VSCode/src/server.scala --- 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 _ => } diff -r 8cac34b3dcd0 -r 31b5a28cadbc src/Tools/VSCode/src/vscode_rendering.scala --- 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) diff -r 8cac34b3dcd0 -r 31b5a28cadbc src/Tools/VSCode/src/vscode_resources.scala --- 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) } )