# HG changeset patch # User wenzelm # Date 1483555328 -3600 # Node ID ca09695eb43c81855bdaf8e8af0dd6ece6fd4744 # Parent 3f20c63f71be95010462a5080a1cdf434380a274 clarified Document.Node.Name (again): canonical platform file; identify document models by native java.io.File; diff -r 3f20c63f71be -r ca09695eb43c src/Pure/General/url.scala --- a/src/Pure/General/url.scala Wed Jan 04 15:20:54 2017 +0100 +++ b/src/Pure/General/url.scala Wed Jan 04 19:42:08 2017 +0100 @@ -52,8 +52,8 @@ /* file URIs */ - def print_file(file: JFile): String = - file.toPath.toAbsolutePath.toUri.normalize.toString + 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 @@ -61,6 +61,6 @@ try { parse_file(uri); true } catch { case _: URISyntaxException | _: IllegalArgumentException => false } - def normalize_file(uri: String): String = - if (is_wellformed_file(uri)) print_file(parse_file(uri)) else uri + def canonical_file(uri: String): JFile = parse_file(uri).getCanonicalFile + def canonical_file_name(uri: String): String = canonical_file(uri).getPath } diff -r 3f20c63f71be -r ca09695eb43c src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Wed Jan 04 15:20:54 2017 +0100 +++ b/src/Pure/Thy/thy_header.scala Wed Jan 04 19:42:08 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 3f20c63f71be -r ca09695eb43c src/Tools/VSCode/src/channel.scala --- a/src/Tools/VSCode/src/channel.scala Wed Jan 04 15:20:54 2017 +0100 +++ b/src/Tools/VSCode/src/channel.scala Wed Jan 04 19:42:08 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 3f20c63f71be -r ca09695eb43c src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Wed Jan 04 15:20:54 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Wed Jan 04 19:42:08 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.parse_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 3f20c63f71be -r ca09695eb43c src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Wed Jan 04 15:20:54 2017 +0100 +++ b/src/Tools/VSCode/src/protocol.scala Wed Jan 04 19:42:08 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 3f20c63f71be -r ca09695eb43c src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Wed Jan 04 15:20:54 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Wed Jan 04 19:42:08 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 3f20c63f71be -r ca09695eb43c src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Jan 04 15:20:54 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Wed Jan 04 19:42:08 2017 +0100 @@ -84,11 +84,11 @@ if Path.is_wellformed(name) } yield { - val file = Path.explode(name).file + val path = Path.explode(name) val opt_text = - try { Some(File.read(file)) } // FIXME content from resources/models + try { Some(File.read(path)) } // FIXME content from resources/models catch { case ERROR(_) => None } - Line.Node_Range(Url.print_file(file), + Line.Node_Range(File.platform_path(path), opt_text match { case Some(text) if range.start > 0 => val chunk = Symbol.Text_Chunk(text) diff -r 3f20c63f71be -r ca09695eb43c src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Wed Jan 04 15:20:54 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Jan 04 19:42:08 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,63 +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 (dir == "" || path.is_absolute) Url.print_file(path.file) + 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.parse_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 = @@ -102,10 +104,12 @@ { 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 + model1 <- + (try { model.update_text(File.read(file)) } + catch { case ERROR(_) => None }) + } yield (file, model1)).toList if (changed_models.isEmpty) (false, st) else (true, st.copy( @@ -129,16 +133,16 @@ val loaded_models = (for { dep <- thy_info.dependencies("", thys).deps.iterator - uri = dep.name.node - if !st.models.isDefinedAt(uri) + file = node_file(dep.name) + if !st.models.isDefinedAt(file) text <- - try { Some(File.read(Url.parse_file(uri))) } + try { Some(File.read(file)) } catch { case ERROR(_) => None } } 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) @@ -159,14 +163,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) }) } @@ -174,7 +178,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) @@ -183,16 +187,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) } )