Skip to content

Commit

Permalink
Merge pull request #578 from UniFormal/master
Browse files Browse the repository at this point in the history
- Core
  - added support for structures defined by morphisms
  - various bug fixes regarding morphisms
  - further maturation of computation algorithm
- jEdit
  - one-step only normalization function
- sTeX
  - complete redesign
  - automatically keeps [RusTeX](https://github.com/slatex/RusTeX) up to date
  - improvements for LSP and the [IDE](https://github.com/slatex/sTeX-IDE)
  - redesigned presentation of sTeX-originated OMDoc, integrated as OMDoc tab in the preview window of the IDE
  - improved error viewer in the IDE
  - co-release with the IDE and sTeX version 3.3 on [CTAN](https://ctan.org/pkg/stex)
- other components
  - new Lean importer
  • Loading branch information
Jazzpirate committed Mar 21, 2023
2 parents 53b293a + 52511ca commit 7fab009
Show file tree
Hide file tree
Showing 159 changed files with 16,430 additions and 8,222 deletions.
18 changes: 11 additions & 7 deletions src/build.sbt
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,7 @@ lazy val src = (project in file(".")).
// This is the main project. 'mmt/deploy' compiles all relevants subprojects, builds a self-contained jar file, and puts into the deploy folder, from where it can be run.
lazy val mmt = (project in file("mmt")).
exclusions(excludedProjects).
dependsOn(stex, pvs, specware, oeis, odk, jedit, latex, openmath, mizar, imps, isabelle, repl, concepts, mathhub, python, intellij, coq, glf, lsp, buildserver).
dependsOn(stex, pvs, specware, oeis, odk, jedit, latex, openmath, mizar, imps, isabelle, repl, concepts, mathhub, python, intellij, coq, lean, glf, lsp, buildserver).
settings(mmtProjectsSettings("mmt"): _*).
settings(
exportJars := false,
Expand Down Expand Up @@ -294,15 +294,19 @@ lazy val coq = (project in file("mmt-coq")).
dependsOn(api, lf).
settings(mmtProjectsSettings("mmt-coq"): _*)

lazy val lean = (project in file("mmt-lean")).
dependsOn(api, lf).
settings(mmtProjectsSettings("mmt-lean"): _*)

lazy val lsp = (project in file("mmt-lsp")).
dependsOn(api,lf).
settings(mmtProjectsSettings("mmt-lsp"): _*).
settings(
libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.14.0",
libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j.websocket" % "0.14.0",
libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.19.0",
libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j.websocket" % "0.19.0",
//libraryDependencies += "org.eclipse.jetty" % "jetty-server" % "11.0.9",
//libraryDependencies += "org.eclipse.jetty" % "jetty-servlet" % "11.0.9",
libraryDependencies += "org.eclipse.jetty.websocket" % "javax-websocket-server-impl" % "9.4.46.v20220331",
libraryDependencies += "org.eclipse.jetty.websocket" % "javax-websocket-server-impl" % "9.4.50.v20221201",
libraryDependencies += "org.scala-lang.modules" %% "scala-java8-compat" % "1.0.2"
)
/*
Expand Down Expand Up @@ -491,19 +495,19 @@ lazy val specware = (project in file("mmt-specware")).

// plugin for reading stex. Maintainer: Dennis
lazy val stex = (project in file("mmt-stex")).
dependsOn(api,odk,lsp).
dependsOn(api,odk,lsp,tiscaf).
settings(
mmtProjectsSettings("mmt-stex"),
libraryDependencies += "org.eclipse.jgit" % "org.eclipse.jgit" % "6.1.0.202203080745-r",
libraryDependencies += "org.slf4j" % "slf4j-simple" % "1.7.30",

Compile / unmanagedJars += baseDirectory.value / "lib" / "lucene-core-9.2.0.jar",
Compile / unmanagedJars += baseDirectory.value / "lib" / "lucene-query-9.2.0.jar",
Compile / unmanagedJars += baseDirectory.value / "lib" / "lucene-queries-9.2.0.jar",
Compile / unmanagedJars += baseDirectory.value / "lib" / "lucene-sandbox-9.2.0.jar",
Compile / unmanagedJars += baseDirectory.value / "lib" / "lucene-queryparser-9.2.0.jar",
Compile / unmanagedJars += baseDirectory.value / "lib" / "lucene-grouping-9.2.0.jar",
Test / unmanagedJars += baseDirectory.value / "lib" / "lucene-core-9.2.0.jar",
Test / unmanagedJars += baseDirectory.value / "lib" / "lucene-query-9.2.0.jar",
Test / unmanagedJars += baseDirectory.value / "lib" / "lucene-queries-9.2.0.jar",
Test / unmanagedJars += baseDirectory.value / "lib" / "lucene-queryparser-9.2.0.jar",
Test / unmanagedJars += baseDirectory.value / "lib" / "lucene-sandbox-9.2.0.jar",
Test / unmanagedJars += baseDirectory.value / "lib" / "lucene-grouping-9.2.0.jar",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ sealed case class Fact(
case Some(valueEqFact) => valueEqFact
case _ => Fact.tryRenderSEquationSystemFact(ref, label, tp = tp, simpleTp = simpleTp, df = df, simpleDf = simpleDf) match {
case Some(equationSystemFact) => equationSystemFact
case _ => SGeneralFact(Some(ref), label, tp, df)
case _ => SGeneralFact(Some(ref), label, tp, simpleDf)
}
}
}
Expand Down
6 changes: 4 additions & 2 deletions src/jEdit-mmt/src/info/kwarc/mmt/jedit/ContextMenu.scala
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,10 @@ class ContextMenu extends DynamicContextMenuService {
val view = jEditTextArea.getView

val menu = new JMenu("MMT")
menu.add(ContextMenu.item("Show Normalization",mmt.editActions.showNormalization(view, false)))
menu.add(ContextMenu.item("Normalize",mmt.editActions.showNormalization(view, true)))
menu.add(ContextMenu.item("Show Full Normalization",mmt.editActions.showNormalization(view, false, true)))
menu.add(ContextMenu.item("Normalize",mmt.editActions.showNormalization(view, true, true)))
menu.add(ContextMenu.item("Show One-Step Normalization",mmt.editActions.showNormalization(view, false, false)))
menu.add(ContextMenu.item("Normalize One Step",mmt.editActions.showNormalization(view, true, false)))
menu.add(ContextMenu.item("Introduce Hole",mmt.editActions.introduceHole(view)))
menu.add(mmt.editActions.viewfindermenu(view))
Array(menu)
Expand Down
4 changes: 2 additions & 2 deletions src/jEdit-mmt/src/info/kwarc/mmt/jedit/EditOperations.scala
Original file line number Diff line number Diff line change
Expand Up @@ -50,12 +50,12 @@ class EditActions(mmtplugin: MMTPlugin) {
*
* @param replace if true, replace selected asset; otherwise, show popup
*/
def showNormalization(view: JEditView, replace: Boolean): Unit = {
def showNormalization(view: JEditView, replace: Boolean, fully: Boolean): Unit = {
val (as, selected) = MMTSideKick.getCurrentAsset(view).getOrElse(return)
as match {
case oa: JObjAsset =>
val obj = oa.obj
val objN = mmtplugin.controller.simplifier(obj, SimplificationUnit(oa.context, true,true, true))
val objN = mmtplugin.controller.simplifier(obj, SimplificationUnit(oa.context, true, true, fully))
val objNS = mmtplugin.asString(objN)
val textArea = view.getTextArea
if (selected && replace) {
Expand Down
4 changes: 2 additions & 2 deletions src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTSideKick.scala
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ class MMTSideKick extends SideKickParser("mmt") with Logger {
TreeBuilder.buildTreeDoc(root, doc)
tree
} catch {
case e: Throwable =>
case e: Exception =>
val msg = e.getClass.toString + ": " + e.getMessage
val pe = ParseError("unknown error: " + msg).setCausedBy(e)
log(msg)
Expand Down Expand Up @@ -177,7 +177,7 @@ object MMTSideKick {
a match {
case m: JAsset =>
asset = Some(m)
m.getEnd.getOffset+1 < end
m.getEnd.getOffset < end
case _ => false
}
}) {
Expand Down
14 changes: 12 additions & 2 deletions src/jEdit-mmt/src/resources/actions.xml
Original file line number Diff line number Diff line change
Expand Up @@ -58,12 +58,22 @@
</ACTION>
<ACTION NAME="mmt-show-normalization">
<CODE>
jEdit.getPlugin("info.kwarc.mmt.jedit.MMTPlugin", true).editActions().showNormalization(view, false);
jEdit.getPlugin("info.kwarc.mmt.jedit.MMTPlugin", true).editActions().showNormalization(view, false, true);
</CODE>
</ACTION>
<ACTION NAME="mmt-normalize-selection">
<CODE>
jEdit.getPlugin("info.kwarc.mmt.jedit.MMTPlugin", true).editActions().showNormalization(view, true);
jEdit.getPlugin("info.kwarc.mmt.jedit.MMTPlugin", true).editActions().showNormalization(view, true, true);
</CODE>
</ACTION>
<ACTION NAME="mmt-show-normalization-onestep">
<CODE>
jEdit.getPlugin("info.kwarc.mmt.jedit.MMTPlugin", true).editActions().showNormalization(view, false, false);
</CODE>
</ACTION>
<ACTION NAME="mmt-normalize-selection-onestep">
<CODE>
jEdit.getPlugin("info.kwarc.mmt.jedit.MMTPlugin", true).editActions().showNormalization(view, true, false);
</CODE>
</ACTION>
</ACTIONS>
2 changes: 2 additions & 0 deletions src/jEdit-mmt/src/resources/mmtplugin.props
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,8 @@ mmt-insert-GS.label=Insert Module Delimiter (MD)
mmt-introduce-hole.label=Introduce hole for expected type
mmt-show-normalization.label=Show normalization
mmt-normalize-selection.label=Normalize selection
mmt-show-normalization-onstep.label=Show one-step normalization
mmt-normalize-selection-onestep.label=Normalize selection one step

# labels for actions defined in browser.actions.xml
mmt-browser-build.label=Build
Expand Down
3 changes: 3 additions & 0 deletions src/mmt-api/resources/mmt-web/buildserver.html
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,9 @@
<ul>
<li ng-repeat="e in queue.finished" ng-class="colorOf(e.result.result)">
{{e.dependency}} {{e.result.result}}
<div ng-if="e.result.result == 'failure'">
<button ng-click="redo(e.taskid)">rebuild</button>
</div>
<span ng-show="e.result.needed.length > 0">missing</span>
<ul>
<li ng-repeat="n in e.result.needed">
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,12 @@ angular.module('buildQueueApp', []).controller('QueueViewer',
$scope.refreshCount = 1;
})
};
$scope.redo = function(id) {
$http.get('/:buildserver/redo?'+id).success(function(data) {
$scope.refreshRate = 1;
$scope.refreshCount = 1;
})
};
$scope.fileName ='';
$scope.make = function() {
var t = $scope.targets.current;
Expand Down
4 changes: 2 additions & 2 deletions src/mmt-api/resources/mmt-web/stex/emptydoc.xhtml
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,6 @@
xmlns:rustex="http://kwarc.info/ns/RusTeX"
lang="en">
<head></head>
<body style="width:614.295px">
<div style="font-size:10.0px;width:345.0px;padding-left:134.64749px;padding-right:134.64749px;line-height:1.2" class="body"></div></body>
<body>
<div style="line-height:1.2;font-size:15px" class="body"></div></body>
</html>
111 changes: 111 additions & 0 deletions src/mmt-api/resources/mmt-web/stex/fonts.css
Original file line number Diff line number Diff line change
@@ -0,0 +1,111 @@
@font-face {
font-family: 'Latin Modern SmallCaps';
font-style: normal;
font-weight: normal;
font-display: swap;
src: url('/stex/fonts/lmromancaps10-regular.otf');
}

@font-face {
font-family: 'Latin Modern SmallCaps';
font-style: italic;
font-weight: normal;
font-display: swap;
src: url('/stex/fonts/lmromancaps10-oblique.otf');
}

@font-face {
font-family: 'Latin Modern';
font-style: normal;
font-weight: normal;
font-display: swap;
src: url('/stex/fonts/lmroman10-regular.otf');
}

@font-face {
font-family: 'Latin Modern';
font-style: italic;
font-weight: normal;
font-display: swap;
src: url('/stex/fonts/lmroman10-italic.otf');
}

@font-face {
font-family: 'Latin Modern';
font-style: normal;
font-weight: bold;
font-display: swap;
src: url('/stex/fonts/lmroman10-bold.otf');
}

@font-face {
font-family: 'Latin Modern';
font-style: italic;
font-weight: bold;
font-display: swap;
src: url('/stex/fonts/lmroman10-bolditalic.otf');
}

@font-face {
font-family: 'Latin Modern Mono';
font-style: normal;
font-weight: normal;
font-display: swap;
src: url('/stex/fonts/lmmono10-regular.otf');
}

@font-face {
font-family: 'Latin Modern Mono';
font-style: italic;
font-weight: normal;
font-display: swap;
src: url('/stex/fonts/lmmono10-italic.otf');
}

@font-face {
font-family: 'Latin Modern Mono';
font-style: normal;
font-weight: bold;
font-display: swap;
src: url('/stex/fonts/lmmonolt10-bold.otf');
}

@font-face {
font-family: 'Latin Modern Mono';
font-style: italic;
font-weight: bold;
font-display: swap;
src: url('/stex/fonts/lmmonolt10-boldoblique.otf');
}

@font-face {
font-family: 'Latin Modern Sans';
font-style: normal;
font-weight: normal;
font-display: swap;
src: url('/stex/fonts/lmsans10-regular.otf');
}

@font-face {
font-family: 'Latin Modern Sans';
font-style: italic;
font-weight: normal;
font-display: swap;
src: url('/stex/fonts/lmsans10-oblique.otf');
}

@font-face {
font-family: 'Latin Modern Sans';
font-style: normal;
font-weight: bold;
font-display: swap;
src: url('/stex/fonts/lmsans10-bold.otf');
}

@font-face {
font-family: 'Latin Modern Sans';
font-style: italic;
font-weight: bold;
font-display: swap;
src: url('/stex/fonts/lmsans10-boldoblique.otf');
}
28 changes: 28 additions & 0 deletions src/mmt-api/resources/mmt-web/stex/fonts/GUST-FONT-LICENSE.TXT
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
% This is version 1.0, dated 22 June 2009, of the GUST Font License.
% (GUST is the Polish TeX Users Group, http://www.gust.org.pl)
%
% For the most recent version of this license see
% http://www.gust.org.pl/fonts/licenses/GUST-FONT-LICENSE.txt
% or
% http://tug.org/fonts/licenses/GUST-FONT-LICENSE.txt
%
% This work may be distributed and/or modified under the conditions
% of the LaTeX Project Public License, either version 1.3c of this
% license or (at your option) any later version.
%
% Please also observe the following clause:
% 1) it is requested, but not legally required, that derived works be
% distributed only after changing the names of the fonts comprising this
% work and given in an accompanying "manifest", and that the
% files comprising the Work, as listed in the manifest, also be given
% new names. Any exceptions to this request are also given in the
% manifest.
%
% We recommend the manifest be given in a separate file named
% MANIFEST-<fontid>.txt, where <fontid> is some unique identification
% of the font family. If a separate "readme" file accompanies the Work,
% we recommend a name of the form README-<fontid>.txt.
%
% The latest version of the LaTeX Project Public License is in
% http://www.latex-project.org/lppl.txt and version 1.3c or later
% is part of all distributions of LaTeX version 2006/05/20 or later.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
6 changes: 6 additions & 0 deletions src/mmt-api/resources/mmt-web/stex/guidedtour.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading

0 comments on commit 7fab009

Please sign in to comment.