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 2320a030cc64e5439b7b900f1b1bffbe0f395893..9c66c1d8827d69bec5cab1994b6481b91df448fa 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/$Opposite$Len.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz index 64e3bf31b209e8bee3c3aff372ec668f6e46d6f6..4be756ef007a97bef120d55489c5a7a911d34bee 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/$Triangle$Problem_$Angle$At$A.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz index d1917f1f9fcc5e33e192b1c2503397b521c71c74..c4d82a42ebe37a7ffcbc74cfd5c94a71decd26c3 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz differ diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz index dc39d7b70440bac5dbcd779c56dad714b7e75851..f7372b2efc222ad5cafc630460f565e28b5dd09d 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz differ diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz index 75610bf6df2298876667f70f2b5fcc1f11f70a89..e47600f8dd1bc6ccd69e4ec3bc2391e2599c7367 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.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 fa23cd6dec26d5f8ea29c1c0e601482e55e6525f..7ee0b0a12463cf21f49a4d914c45cbe1c976d6b1 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/errors/mmt-omdoc/Library/gearbox.mmt.err b/errors/mmt-omdoc/Library/gearbox.mmt.err index 0d566ceee383b6360c3f771b8cf4098de62ac57b..b9e459801db84a8a9028f81eb261036b28ea96b4 100644 --- a/errors/mmt-omdoc/Library/gearbox.mmt.err +++ b/errors/mmt-omdoc/Library/gearbox.mmt.err @@ -10,10 +10,10 @@ <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$15(MMTStructureChecker.scala:374)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element> <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</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 +39,27 @@ <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:263)</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.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element> + <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element> </stacktrace> </error> <error @@ -54,11 +74,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: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>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:316)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13(MMTStructureChecker.scala:325)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13$adapted(MMTStructureChecker.scala:322)</element> <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:319)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:322)</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 +104,27 @@ 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:263)</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.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element> + <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element> </stacktrace> </error> @@ -100,11 +140,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: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>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:316)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13(MMTStructureChecker.scala:325)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13$adapted(MMTStructureChecker.scala:322)</element> <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:319)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:322)</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 +170,27 @@ 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:263)</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.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element> + <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element> </stacktrace> </error> @@ -146,11 +206,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: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>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:316)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13(MMTStructureChecker.scala:325)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13$adapted(MMTStructureChecker.scala:322)</element> <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:319)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:322)</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 +236,27 @@ 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:263)</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.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element> + <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element> </stacktrace> </error> @@ -192,10 +272,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$15(MMTStructureChecker.scala:374)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element> <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</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 +301,27 @@ 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:263)</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.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element> + <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element> </stacktrace> </error> @@ -237,10 +337,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$15(MMTStructureChecker.scala:374)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element> <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</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 +366,27 @@ 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:263)</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.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element> + <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element> </stacktrace> </error> @@ -282,10 +402,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$15(MMTStructureChecker.scala:374)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element> <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</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,7 +431,27 @@ 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:263)</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.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element> + <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element> </stacktrace> </error> @@ -326,10 +466,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$15(MMTStructureChecker.scala:374)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element> <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</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> @@ -355,7 +495,27 @@ 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:263)</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.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element> + <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</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"> @@ -369,10 +529,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$15(MMTStructureChecker.scala:374)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element> <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</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> @@ -398,7 +558,27 @@ 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:263)</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.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element> + <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</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"> @@ -412,10 +592,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$15(MMTStructureChecker.scala:374)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element> <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</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,7 +621,27 @@ 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:263)</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.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element> + <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</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"> @@ -455,10 +655,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$15(MMTStructureChecker.scala:374)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element> <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</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> @@ -484,7 +684,27 @@ 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:263)</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.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element> + <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</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"> @@ -498,10 +718,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$15(MMTStructureChecker.scala:374)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element> <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:350)</element> + <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</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> @@ -527,7 +747,27 @@ 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:263)</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.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element> + <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element> </stacktrace> </error> </errors> diff --git a/narration/Scrolls/TriangleScrolls.omdoc b/narration/Scrolls/TriangleScrolls.omdoc index 92f8e4a48cd6368eb5a72f314d0bea12dc2762a6..fd782e55a48ed1a6e910faba34463623afc98eac 100644 --- a/narration/Scrolls/TriangleScrolls.omdoc +++ b/narration/Scrolls/TriangleScrolls.omdoc @@ -1,5 +1,5 @@ <?xml version="1.0" encoding="UTF-8"?> -<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4946.141.3"/><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><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:47.0.47"/></metadata>Modular scrolls having to do with triangles</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#128.5.0:322.14.0"/></metadata>A blueprint problem theory for triangle scrolls +<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4945.141.3"/><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><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:47.0.47"/></metadata>Modular scrolls having to do with triangles</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#128.5.0:322.14.0"/></metadata>A blueprint problem theory for triangle scrolls B /| / | @@ -9,4 +9,4 @@ (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#324.15.0:345.15.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#497.21.0:653.23.77"/></metadata>A blueprint problem theory for triangle scrolls that require a right angle - We use ?TriangleScroll_GeneralProblem and demand the angle at C to be 90°</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC]" target="http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#655.24.0:690.24.35"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA]" target="http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#988.33.0:1018.33.30"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]" target="http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#1277.42.0:1307.42.30"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?AngleSum]" target="http://mathhub.info/FrameIT/frameworld?AngleSum"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#1521.51.0:1535.51.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?OppositeLen]" target="http://mathhub.info/FrameIT/frameworld?OppositeLen"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#2574.77.0:2591.77.17"/></metadata></mref></omdoc> \ No newline at end of file + We use ?TriangleScroll_GeneralProblem and demand the angle at C to be 90°</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC]" target="http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#655.24.0:690.24.35"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA]" target="http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#987.33.0:1017.33.30"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]" target="http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#1276.42.0:1306.42.30"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?AngleSum]" target="http://mathhub.info/FrameIT/frameworld?AngleSum"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#1520.51.0:1534.51.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?OppositeLen]" target="http://mathhub.info/FrameIT/frameworld?OppositeLen"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#2573.77.0:2590.77.17"/></metadata></mref></omdoc> \ No newline at end of file diff --git a/source/Scrolls/TriangleScrolls.mmt b/source/Scrolls/TriangleScrolls.mmt index 7b4843925f79a59ba38fe2a57a7137d6c57e32fb..ba7b636411aaf27fd1d87ccc9942931a336fe81f 100644 --- a/source/Scrolls/TriangleScrolls.mmt +++ b/source/Scrolls/TriangleScrolls.mmt @@ -26,8 +26,8 @@ theory TriangleProblem_RightAngleAtC = include ?TriangleProblem â™ rightAngleC : ⊦ ( ∠B,C,A ) ≠90.0 ☠- meta ?MetaAnnotations?label s"⊾${lverb C} (${lverb A C} ⟂ ${lverb B C})" ☠- meta ?MetaAnnotations?description s"Right angle at ${lverb C} as enclosed by legs ${lverb A C} and ${lverb B C}." + meta ?MetaAnnotations?label s"⊾${lverb C}" ☠+ meta ?MetaAnnotations?description s"${lverb A C} ⟂ ${lverb B C}: right angle at ${lverb C} as enclosed by legs ${lverb A C} and ${lverb B C}." â™ âš