From 261b160bd6d020d406daad6249b4fe3ac56cda4e Mon Sep 17 00:00:00 2001 From: Florian Rabe Date: Thu, 28 Jul 2016 21:57:54 +0200 Subject: [PATCH] --- src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTSideKick.scala | 2 +- src/jEdit-mmt/src/resources/plugin/properties | 1 + .../src/main/info/kwarc/mmt/api/backend/Backend.scala | 8 ++++++++ 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTSideKick.scala b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTSideKick.scala index f14e7ffbed..9102ef2920 100644 --- a/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTSideKick.scala +++ b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTSideKick.scala @@ -97,7 +97,7 @@ class MMTSideKick extends SideKickParser("mmt") with Logger { val uri = utils.FileURI(path) val text = buffer.getText val nsMap = controller.getNamespaceMap - val ps = controller.backend.resolvePhysical(path) match { + val ps = controller.backend.resolvePhysical(path) orElse controller.backend.resolveAnyPhysicalAndLoad(path) match { case None => ParsingStream.fromString(text, DPath(uri), path.getExtension.getOrElse(""), Some(nsMap)) case Some((a, p)) => diff --git a/src/jEdit-mmt/src/resources/plugin/properties b/src/jEdit-mmt/src/resources/plugin/properties index e6e91b23d4..22ddbea3db 100644 --- a/src/jEdit-mmt/src/resources/plugin/properties +++ b/src/jEdit-mmt/src/resources/plugin/properties @@ -4,5 +4,6 @@ buffer.encoding=UTF-8 view.expandOnInput=true view.wrapGuide=false sidekick-tree.dock-position=left +sidekick.buffer-save-parse=true error-list.dock-position=bottom view.showBufferSwitcher=false diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/backend/Backend.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/backend/Backend.scala index dda7dd6dd4..845d08a02a 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/backend/Backend.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/backend/Backend.scala @@ -212,6 +212,14 @@ class Backend(extman: ExtensionManager, val report: info.kwarc.mmt.api.frontend. } } } + /** like resolveAnyPhysical but automatically loads and returns the archive */ + def resolveAnyPhysicalAndLoad(f: File): Option[(Archive, List[String])] = { + resolveAnyPhysical(f) flatMap { + case (root,rel) => + openArchive(root) + getArchive(root) map {a => (a, rel.tail)} + } + } /** creates and registers a RealizationArchive */ def openRealizationArchive(file: File) {