diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz
index 1e4fe2b8b8cc5f46ea58940a11bc138e79e3f1f3..c3052a5adcb5b18f9e3febaa5659740798f64202 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz
index 5815e8625d0828250cbf7bed52798060475429af..780ac9c58574f888ed2ec00d739fb6c4ff1569da 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz
index 1cc3cf5cc1b3c9e1626d798a72799a658eed5c9d..e11b9e79a43c859c1da4ffeaa6baab5ffa7501db 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz
index 48d3d35101ce8452f38170f7c4f430c0858b4d32..f03c131da820789cf2e3864e0a489ba9804b9cd6 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
index da09733b6672b342a04775053ba91cb1395538a0..4178ed545c97fa640915a6826366829bdd666cc0 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz
index 158099d7784d33707b4c1a4a0754e097a3f9526c..aa5f1057cce4216a00b66e7ed310f44bbbc0c0a8 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz
index 5b56b32d575c9a49378c6f3dbde10356542d6b0a..d1be528881f9dbc458d810b12bc1acfca323e1c8 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz
index b5a1e9adea1d8a5cbf45e6e9225d76ea199ec2f2..727d47f424ded2cfe1924d5558c6475c20a60c69 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.omdoc.xz
index 9a99fa637efac2db63ae26a46b0eec372ea605ce..85e0225877e29e91348ba044384c93bddf54fcb4 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz
index d4d8dc7fc1aed68d20f9a7a09d8171bfebc3fdbd..25f120306c59e0c15ba0449253cc425e892c85bb 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz
index 70e687eb8d08c92c95fcca20b1ae0cf4082324e3..1062d71ff4180da0d295feefa91654e492c0354c 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.omdoc.xz
index 88839abfc4fd6c90d2d1ea8be11e86424da0a226..31ac251318b6324d8b938908aafebcd8a7008f48 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz
index 5128a06d909b5212142a8b93ed1b8682bd2dc144..3e025021bde4bd69c887c3538693b2311fe2721b 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Pushed$Out$Situation$Theory.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Pushed$Out$Situation$Theory.omdoc.xz
new file mode 100644
index 0000000000000000000000000000000000000000..449e4c66f594d1a53d10d155eb5c4e2c1c98f322
Binary files /dev/null and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Pushed$Out$Situation$Theory.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz
index 4305ebcd23f63fbee7f0078b7f653a5e18f36e3c..7153d5370280c5cd6877f518fdbcb446fbbdeda9 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz
index cedfe06f6aac0f8a60f3c3dfb677246af8d442bf..45f5db64c7169e4baba326e4a8196f9122fa2cc6 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Solution.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Solution.omdoc.xz
new file mode 100644
index 0000000000000000000000000000000000000000..55f4158af68d3464a848cb2e067ac66389820e4b
Binary files /dev/null and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Solution.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz
index 42545b9f63fc964af48ccf82b9330e743136817f..23c619eb61e03f9356dbd3a76fe352846a494250 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/cogwheels.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/cogwheels.omdoc.xz
index fa0762b724f45e42764ad4cb9e8aa2f6326a3771..93ddda1944e2f6afcae8e653a62b2c687723da8f 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/cogwheels.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/cogwheels.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz
index d2220ec22192387d63b7116800b7ff95ad7bdefd..a686b8facfa4948f1c28eac573c7836ca29c2b3e 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz
index 25124e91e6f7cd0ddee5d111f9328b07f59b33b4..9f6621b6848a92db866ddfdb24072961f6300f58 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/gearbox.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/gearbox.omdoc.xz
index 23ae774e6648a7f516d796aea2f89d83a69f270a..0a3566337efee4a671bb321e8a92e88c1d7f8be2 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/gearbox.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/gearbox.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/temp.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/temp.omdoc.xz
index 108f6f0558e3a61f4d37c0c693ce7d3928d825a9..dffe9e33af015a62f3dd5d898b5659d57f0c560c 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/temp.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/temp.omdoc.xz differ
diff --git a/errors/mmt-omdoc/Library/gearbox.mmt.err b/errors/mmt-omdoc/Library/gearbox.mmt.err
index 59b932bb0b0d402eac613e271abf644af8aa69ee..b5b3bba9beaffe7d01873380c424c748a1c98cad 100644
--- a/errors/mmt-omdoc/Library/gearbox.mmt.err
+++ b/errors/mmt-omdoc/Library/gearbox.mmt.err
@@ -1,19 +1,14 @@
<errors>
-<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?temp?dist?definition: Judgment |- [p1,p2] : (â„×â„)⟶(â„×â„)⟶â„" level="2">
+<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦∃![m]m^2 â‰((Ï€l p2)-Ï€l p1)^2 -((Ï€r p2)-Ï€r p1)^2 " level="1">
<stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12(RuleBasedChecker.scala:88)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12$adapted(RuleBasedChecker.scala:85)</element>
<element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17(MMTStructureChecker.scala:314)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17$adapted(MMTStructureChecker.scala:290)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:85)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:374)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element>
<element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:290)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
@@ -39,7 +34,85 @@
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
+ <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
+ <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
+ <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.intellij.MMTPluginInterface.handleLine(MMTPlugin.scala:117)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)</element>
+ <element>java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)</element>
+ <element>java.base/java.lang.reflect.Method.invoke(Method.java:566)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror1.jinvokeraw(JavaMirrors.scala:407)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:373)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:389)</element>
+ <element>info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:32)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.method(Plugin.scala:111)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.handleLine(Plugin.scala:122)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.doAction(Shell.scala:39)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.actionPerformed(Shell.scala:34)</element>
+ <element>java.desktop/javax.swing.JTextField.fireActionPerformed(JTextField.java:508)</element>
+ <element>java.desktop/javax.swing.JTextField.postActionEvent(JTextField.java:723)</element>
+ <element>java.desktop/javax.swing.JTextField$NotifyAction.actionPerformed(JTextField.java:839)</element>
+ <element>java.desktop/javax.swing.SwingUtilities.notifyAction(SwingUtilities.java:1810)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBinding(JComponent.java:2903)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBindings(JComponent.java:2951)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyEvent(JComponent.java:2865)</element>
+ <element>java.desktop/java.awt.Component.processEvent(Component.java:6431)</element>
+ <element>java.desktop/java.awt.Container.processEvent(Container.java:2263)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5029)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.KeyboardFocusManager.redispatchEvent(KeyboardFocusManager.java:1950)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchKeyEvent(DefaultKeyboardFocusManager.java:878)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.preDispatchKeyEvent(DefaultKeyboardFocusManager.java:1148)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.typeAheadAssertions(DefaultKeyboardFocusManager.java:1017)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchEvent(DefaultKeyboardFocusManager.java:843)</element>
+ <element>com.intellij.ide.IdeKeyboardFocusManager.dispatchEvent(IdeKeyboardFocusManager.java:41)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:4910)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2773)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:778)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:727)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:751)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:749)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:748)</element>
+ <element>com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:971)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchKeyEvent(IdeEventQueue.java:894)</element>
+ <element>com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:835)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$8(IdeEventQueue.java:452)</element>
+ <element>com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:744)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$9(IdeEventQueue.java:451)</element>
+ <element>com.intellij.openapi.application.impl.ApplicationImpl.runIntendedWriteActionOnCurrentThread(ApplicationImpl.java:802)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:505)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)</element>
</stacktrace>
</error>
<error
@@ -54,11 +127,11 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:263)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:271)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:268)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:313)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13(MMTStructureChecker.scala:322)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13$adapted(MMTStructureChecker.scala:319)</element>
<element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:268)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:319)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
@@ -84,7 +157,85 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
+ <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
+ <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
+ <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.intellij.MMTPluginInterface.handleLine(MMTPlugin.scala:117)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)</element>
+ <element>java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)</element>
+ <element>java.base/java.lang.reflect.Method.invoke(Method.java:566)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror1.jinvokeraw(JavaMirrors.scala:407)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:373)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:389)</element>
+ <element>info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:32)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.method(Plugin.scala:111)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.handleLine(Plugin.scala:122)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.doAction(Shell.scala:39)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.actionPerformed(Shell.scala:34)</element>
+ <element>java.desktop/javax.swing.JTextField.fireActionPerformed(JTextField.java:508)</element>
+ <element>java.desktop/javax.swing.JTextField.postActionEvent(JTextField.java:723)</element>
+ <element>java.desktop/javax.swing.JTextField$NotifyAction.actionPerformed(JTextField.java:839)</element>
+ <element>java.desktop/javax.swing.SwingUtilities.notifyAction(SwingUtilities.java:1810)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBinding(JComponent.java:2903)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBindings(JComponent.java:2951)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyEvent(JComponent.java:2865)</element>
+ <element>java.desktop/java.awt.Component.processEvent(Component.java:6431)</element>
+ <element>java.desktop/java.awt.Container.processEvent(Container.java:2263)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5029)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.KeyboardFocusManager.redispatchEvent(KeyboardFocusManager.java:1950)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchKeyEvent(DefaultKeyboardFocusManager.java:878)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.preDispatchKeyEvent(DefaultKeyboardFocusManager.java:1148)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.typeAheadAssertions(DefaultKeyboardFocusManager.java:1017)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchEvent(DefaultKeyboardFocusManager.java:843)</element>
+ <element>com.intellij.ide.IdeKeyboardFocusManager.dispatchEvent(IdeKeyboardFocusManager.java:41)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:4910)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2773)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:778)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:727)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:751)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:749)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:748)</element>
+ <element>com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:971)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchKeyEvent(IdeEventQueue.java:894)</element>
+ <element>com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:835)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$8(IdeEventQueue.java:452)</element>
+ <element>com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:744)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$9(IdeEventQueue.java:451)</element>
+ <element>com.intellij.openapi.application.impl.ApplicationImpl.runIntendedWriteActionOnCurrentThread(ApplicationImpl.java:802)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:505)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)</element>
</stacktrace>
</error>
@@ -100,11 +251,11 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:263)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:271)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:268)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:313)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13(MMTStructureChecker.scala:322)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13$adapted(MMTStructureChecker.scala:319)</element>
<element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:268)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:319)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
@@ -130,7 +281,85 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
+ <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
+ <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
+ <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.intellij.MMTPluginInterface.handleLine(MMTPlugin.scala:117)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)</element>
+ <element>java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)</element>
+ <element>java.base/java.lang.reflect.Method.invoke(Method.java:566)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror1.jinvokeraw(JavaMirrors.scala:407)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:373)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:389)</element>
+ <element>info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:32)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.method(Plugin.scala:111)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.handleLine(Plugin.scala:122)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.doAction(Shell.scala:39)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.actionPerformed(Shell.scala:34)</element>
+ <element>java.desktop/javax.swing.JTextField.fireActionPerformed(JTextField.java:508)</element>
+ <element>java.desktop/javax.swing.JTextField.postActionEvent(JTextField.java:723)</element>
+ <element>java.desktop/javax.swing.JTextField$NotifyAction.actionPerformed(JTextField.java:839)</element>
+ <element>java.desktop/javax.swing.SwingUtilities.notifyAction(SwingUtilities.java:1810)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBinding(JComponent.java:2903)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBindings(JComponent.java:2951)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyEvent(JComponent.java:2865)</element>
+ <element>java.desktop/java.awt.Component.processEvent(Component.java:6431)</element>
+ <element>java.desktop/java.awt.Container.processEvent(Container.java:2263)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5029)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.KeyboardFocusManager.redispatchEvent(KeyboardFocusManager.java:1950)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchKeyEvent(DefaultKeyboardFocusManager.java:878)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.preDispatchKeyEvent(DefaultKeyboardFocusManager.java:1148)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.typeAheadAssertions(DefaultKeyboardFocusManager.java:1017)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchEvent(DefaultKeyboardFocusManager.java:843)</element>
+ <element>com.intellij.ide.IdeKeyboardFocusManager.dispatchEvent(IdeKeyboardFocusManager.java:41)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:4910)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2773)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:778)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:727)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:751)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:749)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:748)</element>
+ <element>com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:971)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchKeyEvent(IdeEventQueue.java:894)</element>
+ <element>com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:835)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$8(IdeEventQueue.java:452)</element>
+ <element>com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:744)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$9(IdeEventQueue.java:451)</element>
+ <element>com.intellij.openapi.application.impl.ApplicationImpl.runIntendedWriteActionOnCurrentThread(ApplicationImpl.java:802)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:505)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)</element>
</stacktrace>
</error>
@@ -146,11 +375,11 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:263)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:271)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:268)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:313)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13(MMTStructureChecker.scala:322)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13$adapted(MMTStructureChecker.scala:319)</element>
<element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:268)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:319)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
@@ -176,7 +405,85 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
+ <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
+ <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
+ <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.intellij.MMTPluginInterface.handleLine(MMTPlugin.scala:117)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)</element>
+ <element>java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)</element>
+ <element>java.base/java.lang.reflect.Method.invoke(Method.java:566)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror1.jinvokeraw(JavaMirrors.scala:407)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:373)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:389)</element>
+ <element>info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:32)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.method(Plugin.scala:111)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.handleLine(Plugin.scala:122)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.doAction(Shell.scala:39)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.actionPerformed(Shell.scala:34)</element>
+ <element>java.desktop/javax.swing.JTextField.fireActionPerformed(JTextField.java:508)</element>
+ <element>java.desktop/javax.swing.JTextField.postActionEvent(JTextField.java:723)</element>
+ <element>java.desktop/javax.swing.JTextField$NotifyAction.actionPerformed(JTextField.java:839)</element>
+ <element>java.desktop/javax.swing.SwingUtilities.notifyAction(SwingUtilities.java:1810)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBinding(JComponent.java:2903)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBindings(JComponent.java:2951)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyEvent(JComponent.java:2865)</element>
+ <element>java.desktop/java.awt.Component.processEvent(Component.java:6431)</element>
+ <element>java.desktop/java.awt.Container.processEvent(Container.java:2263)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5029)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.KeyboardFocusManager.redispatchEvent(KeyboardFocusManager.java:1950)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchKeyEvent(DefaultKeyboardFocusManager.java:878)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.preDispatchKeyEvent(DefaultKeyboardFocusManager.java:1148)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.typeAheadAssertions(DefaultKeyboardFocusManager.java:1017)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchEvent(DefaultKeyboardFocusManager.java:843)</element>
+ <element>com.intellij.ide.IdeKeyboardFocusManager.dispatchEvent(IdeKeyboardFocusManager.java:41)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:4910)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2773)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:778)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:727)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:751)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:749)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:748)</element>
+ <element>com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:971)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchKeyEvent(IdeEventQueue.java:894)</element>
+ <element>com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:835)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$8(IdeEventQueue.java:452)</element>
+ <element>com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:744)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$9(IdeEventQueue.java:451)</element>
+ <element>com.intellij.openapi.application.impl.ApplicationImpl.runIntendedWriteActionOnCurrentThread(ApplicationImpl.java:802)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:505)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)</element>
</stacktrace>
</error>
@@ -192,10 +499,10 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17(MMTStructureChecker.scala:314)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17$adapted(MMTStructureChecker.scala:290)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:374)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element>
<element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:290)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
@@ -221,7 +528,85 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
+ <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
+ <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
+ <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.intellij.MMTPluginInterface.handleLine(MMTPlugin.scala:117)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)</element>
+ <element>java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)</element>
+ <element>java.base/java.lang.reflect.Method.invoke(Method.java:566)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror1.jinvokeraw(JavaMirrors.scala:407)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:373)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:389)</element>
+ <element>info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:32)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.method(Plugin.scala:111)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.handleLine(Plugin.scala:122)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.doAction(Shell.scala:39)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.actionPerformed(Shell.scala:34)</element>
+ <element>java.desktop/javax.swing.JTextField.fireActionPerformed(JTextField.java:508)</element>
+ <element>java.desktop/javax.swing.JTextField.postActionEvent(JTextField.java:723)</element>
+ <element>java.desktop/javax.swing.JTextField$NotifyAction.actionPerformed(JTextField.java:839)</element>
+ <element>java.desktop/javax.swing.SwingUtilities.notifyAction(SwingUtilities.java:1810)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBinding(JComponent.java:2903)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBindings(JComponent.java:2951)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyEvent(JComponent.java:2865)</element>
+ <element>java.desktop/java.awt.Component.processEvent(Component.java:6431)</element>
+ <element>java.desktop/java.awt.Container.processEvent(Container.java:2263)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5029)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.KeyboardFocusManager.redispatchEvent(KeyboardFocusManager.java:1950)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchKeyEvent(DefaultKeyboardFocusManager.java:878)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.preDispatchKeyEvent(DefaultKeyboardFocusManager.java:1148)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.typeAheadAssertions(DefaultKeyboardFocusManager.java:1017)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchEvent(DefaultKeyboardFocusManager.java:843)</element>
+ <element>com.intellij.ide.IdeKeyboardFocusManager.dispatchEvent(IdeKeyboardFocusManager.java:41)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:4910)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2773)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:778)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:727)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:751)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:749)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:748)</element>
+ <element>com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:971)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchKeyEvent(IdeEventQueue.java:894)</element>
+ <element>com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:835)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$8(IdeEventQueue.java:452)</element>
+ <element>com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:744)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$9(IdeEventQueue.java:451)</element>
+ <element>com.intellij.openapi.application.impl.ApplicationImpl.runIntendedWriteActionOnCurrentThread(ApplicationImpl.java:802)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:505)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)</element>
</stacktrace>
</error>
@@ -237,10 +622,10 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17(MMTStructureChecker.scala:314)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17$adapted(MMTStructureChecker.scala:290)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:374)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element>
<element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:290)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
@@ -266,7 +651,85 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
+ <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
+ <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
+ <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.intellij.MMTPluginInterface.handleLine(MMTPlugin.scala:117)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)</element>
+ <element>java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)</element>
+ <element>java.base/java.lang.reflect.Method.invoke(Method.java:566)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror1.jinvokeraw(JavaMirrors.scala:407)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:373)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:389)</element>
+ <element>info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:32)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.method(Plugin.scala:111)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.handleLine(Plugin.scala:122)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.doAction(Shell.scala:39)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.actionPerformed(Shell.scala:34)</element>
+ <element>java.desktop/javax.swing.JTextField.fireActionPerformed(JTextField.java:508)</element>
+ <element>java.desktop/javax.swing.JTextField.postActionEvent(JTextField.java:723)</element>
+ <element>java.desktop/javax.swing.JTextField$NotifyAction.actionPerformed(JTextField.java:839)</element>
+ <element>java.desktop/javax.swing.SwingUtilities.notifyAction(SwingUtilities.java:1810)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBinding(JComponent.java:2903)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBindings(JComponent.java:2951)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyEvent(JComponent.java:2865)</element>
+ <element>java.desktop/java.awt.Component.processEvent(Component.java:6431)</element>
+ <element>java.desktop/java.awt.Container.processEvent(Container.java:2263)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5029)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.KeyboardFocusManager.redispatchEvent(KeyboardFocusManager.java:1950)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchKeyEvent(DefaultKeyboardFocusManager.java:878)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.preDispatchKeyEvent(DefaultKeyboardFocusManager.java:1148)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.typeAheadAssertions(DefaultKeyboardFocusManager.java:1017)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchEvent(DefaultKeyboardFocusManager.java:843)</element>
+ <element>com.intellij.ide.IdeKeyboardFocusManager.dispatchEvent(IdeKeyboardFocusManager.java:41)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:4910)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2773)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:778)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:727)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:751)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:749)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:748)</element>
+ <element>com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:971)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchKeyEvent(IdeEventQueue.java:894)</element>
+ <element>com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:835)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$8(IdeEventQueue.java:452)</element>
+ <element>com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:744)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$9(IdeEventQueue.java:451)</element>
+ <element>com.intellij.openapi.application.impl.ApplicationImpl.runIntendedWriteActionOnCurrentThread(ApplicationImpl.java:802)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:505)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)</element>
</stacktrace>
</error>
@@ -282,10 +745,10 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17(MMTStructureChecker.scala:314)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17$adapted(MMTStructureChecker.scala:290)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:374)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element>
<element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:290)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
@@ -311,96 +774,88 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
- </stacktrace>
-</error>
-
-<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?c2?definition: Judgment |- ['center=⟨0,2⟩,radius=1,numteeth=10,angle=0.05'] : cogwheel" level="2">
- <stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
<element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17(MMTStructureChecker.scala:314)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17$adapted(MMTStructureChecker.scala:290)</element>
- <element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:290)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element>
- <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element>
- <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
- </stacktrace>
-</error>
-<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?c2?definition: Judgment |- ['center=⟨0,2⟩,radius=1,numteeth=10,angle=0.05'] : cogwheel" level="2">
- <stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
+ <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
<element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17(MMTStructureChecker.scala:314)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17$adapted(MMTStructureChecker.scala:290)</element>
- <element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:290)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element>
- <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element>
- <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.intellij.MMTPluginInterface.handleLine(MMTPlugin.scala:117)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)</element>
+ <element>java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)</element>
+ <element>java.base/java.lang.reflect.Method.invoke(Method.java:566)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror1.jinvokeraw(JavaMirrors.scala:407)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:373)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:389)</element>
+ <element>info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:32)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.method(Plugin.scala:111)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.handleLine(Plugin.scala:122)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.doAction(Shell.scala:39)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.actionPerformed(Shell.scala:34)</element>
+ <element>java.desktop/javax.swing.JTextField.fireActionPerformed(JTextField.java:508)</element>
+ <element>java.desktop/javax.swing.JTextField.postActionEvent(JTextField.java:723)</element>
+ <element>java.desktop/javax.swing.JTextField$NotifyAction.actionPerformed(JTextField.java:839)</element>
+ <element>java.desktop/javax.swing.SwingUtilities.notifyAction(SwingUtilities.java:1810)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBinding(JComponent.java:2903)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBindings(JComponent.java:2951)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyEvent(JComponent.java:2865)</element>
+ <element>java.desktop/java.awt.Component.processEvent(Component.java:6431)</element>
+ <element>java.desktop/java.awt.Container.processEvent(Container.java:2263)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5029)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.KeyboardFocusManager.redispatchEvent(KeyboardFocusManager.java:1950)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchKeyEvent(DefaultKeyboardFocusManager.java:878)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.preDispatchKeyEvent(DefaultKeyboardFocusManager.java:1148)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.typeAheadAssertions(DefaultKeyboardFocusManager.java:1017)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchEvent(DefaultKeyboardFocusManager.java:843)</element>
+ <element>com.intellij.ide.IdeKeyboardFocusManager.dispatchEvent(IdeKeyboardFocusManager.java:41)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:4910)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2773)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:778)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:727)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:751)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:749)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:748)</element>
+ <element>com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:971)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchKeyEvent(IdeEventQueue.java:894)</element>
+ <element>com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:835)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$8(IdeEventQueue.java:452)</element>
+ <element>com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:744)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$9(IdeEventQueue.java:451)</element>
+ <element>com.intellij.openapi.application.impl.ApplicationImpl.runIntendedWriteActionOnCurrentThread(ApplicationImpl.java:802)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:505)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)</element>
</stacktrace>
</error>
+
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?definition: Judgment |- eq_refl c1.radius+c2.radius : ⊦interlocking c1 c2" level="2">
<stacktrace>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
@@ -412,10 +867,10 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17(MMTStructureChecker.scala:314)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17$adapted(MMTStructureChecker.scala:290)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:374)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element>
<element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:290)</element>
+ <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
@@ -441,93 +896,85 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
- </stacktrace>
-</error>
-<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?definition: Judgment |- eq_refl c1.radius+c2.radius : ⊦interlocking c1 c2" level="2">
- <stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
<element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17(MMTStructureChecker.scala:314)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17$adapted(MMTStructureChecker.scala:290)</element>
- <element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:290)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element>
- <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element>
- <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
- </stacktrace>
-</error>
-<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?definition: Judgment |- eq_refl c1.radius+c2.radius : ⊦interlocking c1 c2" level="2">
- <stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
+ <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
+ <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
+ <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
<element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17(MMTStructureChecker.scala:314)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17$adapted(MMTStructureChecker.scala:290)</element>
- <element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:290)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element>
- <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element>
- <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.intellij.MMTPluginInterface.handleLine(MMTPlugin.scala:117)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)</element>
+ <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)</element>
+ <element>java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)</element>
+ <element>java.base/java.lang.reflect.Method.invoke(Method.java:566)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror1.jinvokeraw(JavaMirrors.scala:407)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:373)</element>
+ <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:389)</element>
+ <element>info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:32)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.method(Plugin.scala:111)</element>
+ <element>info.kwarc.mmt.intellij.MMTJar.handleLine(Plugin.scala:122)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.doAction(Shell.scala:39)</element>
+ <element>info.kwarc.mmt.intellij.ui.ShellViewer.actionPerformed(Shell.scala:34)</element>
+ <element>java.desktop/javax.swing.JTextField.fireActionPerformed(JTextField.java:508)</element>
+ <element>java.desktop/javax.swing.JTextField.postActionEvent(JTextField.java:723)</element>
+ <element>java.desktop/javax.swing.JTextField$NotifyAction.actionPerformed(JTextField.java:839)</element>
+ <element>java.desktop/javax.swing.SwingUtilities.notifyAction(SwingUtilities.java:1810)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBinding(JComponent.java:2903)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyBindings(JComponent.java:2951)</element>
+ <element>java.desktop/javax.swing.JComponent.processKeyEvent(JComponent.java:2865)</element>
+ <element>java.desktop/java.awt.Component.processEvent(Component.java:6431)</element>
+ <element>java.desktop/java.awt.Container.processEvent(Container.java:2263)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5029)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.KeyboardFocusManager.redispatchEvent(KeyboardFocusManager.java:1950)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchKeyEvent(DefaultKeyboardFocusManager.java:878)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.preDispatchKeyEvent(DefaultKeyboardFocusManager.java:1148)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.typeAheadAssertions(DefaultKeyboardFocusManager.java:1017)</element>
+ <element>java.desktop/java.awt.DefaultKeyboardFocusManager.dispatchEvent(DefaultKeyboardFocusManager.java:843)</element>
+ <element>com.intellij.ide.IdeKeyboardFocusManager.dispatchEvent(IdeKeyboardFocusManager.java:41)</element>
+ <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:4910)</element>
+ <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+ <element>java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2773)</element>
+ <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4861)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:778)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:727)</element>
+ <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:751)</element>
+ <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:749)</element>
+ <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+ <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+ <element>java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:748)</element>
+ <element>com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:971)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchKeyEvent(IdeEventQueue.java:894)</element>
+ <element>com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:835)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$8(IdeEventQueue.java:452)</element>
+ <element>com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:744)</element>
+ <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$9(IdeEventQueue.java:451)</element>
+ <element>com.intellij.openapi.application.impl.ApplicationImpl.runIntendedWriteActionOnCurrentThread(ApplicationImpl.java:802)</element>
+ <element>com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:505)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)</element>
+ <element>java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)</element>
</stacktrace>
</error>
</errors>
diff --git a/narration/IntegrationTests/SituationTheory.omdoc b/narration/IntegrationTests/SituationTheory.omdoc
index f6ce7cc4ef996431f7c0d896082cce0ff57cab3e..8030e5412885174306e58fb77688c143be28f0e5 100644
--- a/narration/IntegrationTests/SituationTheory.omdoc
+++ b/narration/IntegrationTests/SituationTheory.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#0.0.0:1966.78.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld/integrationtests"/><instruction text="import frameworld http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#194.6.0:220.6.26"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#1535.56.0:1549.56.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#1661.64.0:1681.64.20"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#0.0.0:1962.78.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld/integrationtests"/><instruction text="import frameworld http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#194.6.0:220.6.26"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#1535.56.0:1549.56.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#1661.64.0:1681.64.20"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/MetaTheories.omdoc b/narration/MetaTheories.omdoc
index a75d096ac0d47212c0f5963561f4ffb33343746b..bb10aba7599ba72d770f36e54f91b7e0336eb65e 100644
--- a/narration/MetaTheories.omdoc
+++ b/narration/MetaTheories.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:1074.34.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#70.4.0:198.4.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#200.5.0:221.5.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#628.22.0:723.22.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#725.23.0:745.23.20"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:1072.33.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#70.4.0:198.4.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#200.5.0:221.5.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#628.22.0:723.22.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#725.23.0:745.23.20"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Pushed$Out$Situation$Theory.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Pushed$Out$Situation$Theory.rel
new file mode 100644
index 0000000000000000000000000000000000000000..46620426124295e949be623cdf9e0a605ab4050c
--- /dev/null
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Pushed$Out$Situation$Theory.rel
@@ -0,0 +1,2 @@
+theory http://mathhub.info/FrameIT/frameworld/integrationtests?PushedOutSituationTheory
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?PushedOutSituationTheory http://mathhub.info/FrameIT/frameworld?FrameworldMeta
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Solution.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Solution.rel
new file mode 100644
index 0000000000000000000000000000000000000000..9040530d2621f36e6142b30fec69e5244b0e0ef9
--- /dev/null
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Solution.rel
@@ -0,0 +1,2 @@
+theory http://mathhub.info/FrameIT/frameworld/integrationtests?Solution
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/cogwheels.rel b/relational/http..mathhub.info/LoViVo/gearbox/cogwheels.rel
index 3aa05d239ee890672ec53103c74d83e0547f72e8..18715a350767df6634ca85bd70e0bd8e1b0146c5 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/cogwheels.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/cogwheels.rel
@@ -21,9 +21,6 @@ constant http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?angle
DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?angle?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/LoViVo/gearbox?cogwheels http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel
constant http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/LoViVo/gearbox?cogwheels http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel_theory
theory http://mathhub.info/LoViVo/gearbox?cogwheels/rotating_cogwheel_theory
HasMeta http://mathhub.info/LoViVo/gearbox?cogwheels/rotating_cogwheel_theory http://mathhub.info/MitM/Foundation?Logic
@@ -36,6 +33,3 @@ constant http://mathhub.info/LoViVo/gearbox?cogwheels/rotating_cogwheel_theory?a
DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels/rotating_cogwheel_theory?angular_force?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/LoViVo/gearbox?cogwheels http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel
constant http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel b/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
index 9eec5e1a8a588435994a704fe7c057710e4aa454..ee58104abfa6e6176a7d8aa8ac9c944767d2b1b2 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
@@ -15,6 +15,11 @@ Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearb
constant http://mathhub.info/LoViVo/gearbox?gb2?c2
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://cds.omdoc.org/urtheories?NatSymbols?NAT?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking
constant http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?prop?type
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/gearbox.rel b/relational/http..mathhub.info/LoViVo/gearbox/gearbox.rel
index ef6aadb1478ef6a41dbc6ec2145e273b07acd2ef..9c1f4a34791a6a2b580541b74f569256f4f0aa57 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/gearbox.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/gearbox.rel
@@ -35,11 +35,9 @@ DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?implies?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?forall?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?eq?type
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/temp.rel b/relational/http..mathhub.info/LoViVo/gearbox/temp.rel
index 18ae45a45e9c0e4dd4307e6319d2974d762757da..7b51cc248325726aa705dc2ef42067ee49ec1439 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/temp.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/temp.rel
@@ -6,3 +6,18 @@ Includes http://mathhub.info/LoViVo/gearbox?temp http://mathhub.info/MitM/Founda
Declares http://mathhub.info/LoViVo/gearbox?temp http://mathhub.info/LoViVo/gearbox?temp?dist
constant http://mathhub.info/LoViVo/gearbox?temp?dist
DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?squareRoot?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?exponentiation?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
diff --git a/source/IntegrationTests/SituationTheory.mmt b/source/IntegrationTests/SituationTheory.mmt
index 8633382500516bea135bc43f67423ec8145e1185..bc4e894059eaf8a2fa0665fee2d8d16c30fd0f31 100644
--- a/source/IntegrationTests/SituationTheory.mmt
+++ b/source/IntegrationTests/SituationTheory.mmt
@@ -66,6 +66,7 @@ theory SituationSpace =
theory RootSituationTheory =
include ?MyScroll â™
b: type â™
+ p : point ☠= ⟨0.0, 0.0, 0.0⟩ â™
view v : ?MyScroll/Problem -> ?SituationSpace/RootSituationTheory =
a = b â™
@@ -75,5 +76,6 @@ theory SituationSpace =
theory PushedOutSituationTheory =
include ?SituationSpace/RootSituationTheory â™
c: type ☠= b â™
+ q = p â™
âš
âš
\ No newline at end of file