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 373c9a260b4e9b0792b8ea06a8ea2762f93aa153..71042ec64dcd2d628c4fbfd128844e392f662811 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 c6dde2467378c5ff4a036bb06d56e27ede374ea1..afd90f697c89d845f7f3ccecbc0fcae9f7029389 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 ff8d073b773284c7c3fb28332444012bca6d6e92..70d82f162407d7e4972b797ab9c3dcb0d644453e 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/$Opposite$Len.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
index 5fe56876ee69f53b81ecdc065f92dc74cdfa704e..a5a882abc1cfad4cc35f3263d5f9e48ee0e01964 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/$Pythagoras.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Pythagoras.omdoc.xz
index 1c29455b911de928123dd7f7b2448a7a48e23e69..220acb5aaf530ad737af2ef4d70c27cecbb7d427 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Pythagoras.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Pythagoras.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 4ec13830ea8b25ebcfd3c77e538a5ba3d4f96248..c2c96a06e1e46ffb8de29265790a98cc012b8752 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 1ff184df7047ab5d68a942b06e2b1cd91e7b30da..c549a1d9ed0db2f21638365c291c43d0c72b5187 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/$Sample$Situation$Theory.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.omdoc.xz
index 318f4e27bbde5a4ab5ed0a1fcabce6c18e630af5..b50e33a2fb6a16b5bd16f65b081f013d5312e3ab 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.omdoc.xz differ
diff --git a/errors/mmt-omdoc/MetaTheories.mmt.err b/errors/mmt-omdoc/MetaTheories.mmt.err
index a003a310ddaac2945e140ceaaaa6d7e3db90d6b4..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/errors/mmt-omdoc/MetaTheories.mmt.err
+++ b/errors/mmt-omdoc/MetaTheories.mmt.err
@@ -1,2 +0,0 @@
-<errors>
-</errors>
diff --git a/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err b/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
index b94e29a816df7d8bc3b6948eed8d82cb23ae7315..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
+++ b/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
@@ -1,241 +0,0 @@
-<errors>
-<error
-type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition: Judgment |- ⟨,sketch "By Pythagora's theorem"⟩ : Σ x:â„.⊦d- A Bâ‰x" 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>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.readInModuleAux(StructureParser.scala:587)</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.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.ServerEndpoints$.$anonfun$listScrolls$1(ServerEndpoints.scala:134)</element>
- <element>io.finch.internal.HighPriorityMapperConversions.$anonfun$mapperFromOutputValue$2(Mapper.scala:82)</element>
- <element>io.finch.Endpoint.$anonfun$mapOutput$2(Endpoint.scala:102)</element>
- <element>cats.ApplicativeError.catchNonFatal(ApplicativeError.scala:203)</element>
- <element>cats.ApplicativeError.catchNonFatal$(ApplicativeError.scala:202)</element>
- <element>cats.effect.IOLowPriorityInstances$IOEffect.catchNonFatal(IO.scala:767)</element>
- <element>io.finch.Endpoint.$anonfun$mapOutput$1(Endpoint.scala:102)</element>
- <element>io.finch.Output.traverseFlatten(Output.scala:57)</element>
- <element>io.finch.Output.traverseFlatten$(Output.scala:55)</element>
- <element>io.finch.Output$Payload.traverseFlatten(Output.scala:141)</element>
- <element>io.finch.Endpoint$$anon$25.apply(Endpoint.scala:109)</element>
- <element>io.finch.Endpoint$$anon$25.apply(Endpoint.scala:108)</element>
- <element>cats.effect.internals.IORunLoop$.cats$effect$internals$IORunLoop$$loop(IORunLoop.scala:139)</element>
- <element>cats.effect.internals.IORunLoop$.start(IORunLoop.scala:34)</element>
- <element>cats.effect.IO.unsafeRunAsync(IO.scala:257)</element>
- <element>cats.effect.IO.$anonfun$runAsync$1(IO.scala:177)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>cats.effect.internals.IORunLoop$.step(IORunLoop.scala:185)</element>
- <element>cats.effect.IO.unsafeRunTimed(IO.scala:320)</element>
- <element>cats.effect.IO.unsafeRunSync(IO.scala:239)</element>
- <element>cats.effect.SyncIO.unsafeRunSync(SyncIO.scala:48)</element>
- <element>io.finch.ToService.apply(ToService.scala:33)</element>
- <element>io.finch.ToService.apply(ToService.scala:12)</element>
- <element>com.twitter.finagle.ServiceProxy.apply(ServiceProxy.scala:12)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.tracing.AnnotatingTracingFilter.apply(TraceInitializerFilter.scala:142)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.tracing.ServerDestTracingFilter.apply(DestinationTracing.scala:54)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.service.DeadlineFilter.apply(DeadlineFilter.scala:267)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.filter.ExceptionSourceFilter.apply(ExceptionSourceFilter.scala:50)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.filter.MkJvmFilter$$anon$1.apply(MkJvmFilter.scala:30)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.tracing.AnnotatingTracingFilter.apply(TraceInitializerFilter.scala:142)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.http.filter.HttpNackFilter.apply(HttpNackFilter.scala:156)</element>
- <element>com.twitter.finagle.http.filter.HttpNackFilter.apply(HttpNackFilter.scala:113)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.http.filter.PayloadSizeFilter.apply(PayloadSizeFilter.scala:123)</element>
- <element>com.twitter.finagle.http.filter.PayloadSizeFilter.apply(PayloadSizeFilter.scala:47)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.server.BackupRequest$$anon$1$$anon$2.apply(BackupRequest.scala:31)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.http.filter.ServerContextFilter.$anonfun$apply$1(ContextFilter.scala:15)</element>
- <element>com.twitter.util.Local.let(Local.scala:4978)</element>
- <element>com.twitter.finagle.context.MarshalledContext.letLocal(MarshalledContext.scala:157)</element>
- <element>com.twitter.finagle.context.MarshalledContext.let(MarshalledContext.scala:104)</element>
- <element>com.twitter.finagle.http.codec.context.HttpContext$.read(HttpContext.scala:114)</element>
- <element>com.twitter.finagle.http.filter.ServerContextFilter.apply(ContextFilter.scala:15)</element>
- <element>com.twitter.finagle.http.filter.ServerContextFilter.apply(ContextFilter.scala:12)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:13)</element>
- <element>com.twitter.finagle.http.HttpServerTraceInitializer.$anonfun$make$3(HttpServerTraceInitializer.scala:20)</element>
- <element>com.twitter.finagle.http.TraceInfo$.$anonfun$letTraceIdFromRequestHeaders$1(TraceInfo.scala:105)</element>
- <element>com.twitter.util.Local.let(Local.scala:4978)</element>
- <element>com.twitter.finagle.context.MarshalledContext.letLocal(MarshalledContext.scala:157)</element>
- <element>com.twitter.finagle.context.MarshalledContext.let(MarshalledContext.scala:90)</element>
- <element>com.twitter.finagle.tracing.Trace$.letId(Trace.scala:104)</element>
- <element>com.twitter.finagle.http.TraceInfo$.letTraceIdFromRequestHeaders(TraceInfo.scala:103)</element>
- <element>com.twitter.finagle.http.HttpServerTraceInitializer.$anonfun$make$2(HttpServerTraceInitializer.scala:20)</element>
- <element>com.twitter.util.Local.let(Local.scala:4978)</element>
- <element>com.twitter.finagle.context.LocalContext.letLocal(LocalContext.scala:51)</element>
- <element>com.twitter.finagle.context.LocalContext.let(LocalContext.scala:24)</element>
- <element>com.twitter.finagle.tracing.Trace$.letTracer(Trace.scala:124)</element>
- <element>com.twitter.finagle.http.HttpServerTraceInitializer.$anonfun$make$1(HttpServerTraceInitializer.scala:20)</element>
- <element>com.twitter.finagle.Filter$$anon$16.apply(Filter.scala:406)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.filter.MonitorFilter.apply(MonitorFilter.scala:66)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.http.filter.DtabFilter.apply(DtabFilter.scala:25)</element>
- <element>com.twitter.finagle.http.filter.DtabFilter.apply(DtabFilter.scala:12)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element>
- <element>com.twitter.finagle.http.codec.ResponseConformanceFilter$.apply(ResponseConformanceFilter.scala:23)</element>
- <element>com.twitter.finagle.http.codec.ResponseConformanceFilter$.apply(ResponseConformanceFilter.scala:18)</element>
- <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element>
- <element>com.twitter.finagle.http.codec.HttpServerDispatcher.dispatch(HttpServerDispatcher.scala:42)</element>
- <element>com.twitter.finagle.http.codec.HttpServerDispatcher.dispatch(HttpServerDispatcher.scala:23)</element>
- <element>com.twitter.finagle.http.exp.GenStreamingSerialServerDispatcher.$anonfun$dispatchAndHandleFn$2(GenStreamingSerialServerDispatcher.scala:83)</element>
- <element>com.twitter.util.Local.let(Local.scala:4978)</element>
- <element>com.twitter.finagle.context.LocalContext.letLocal(LocalContext.scala:51)</element>
- <element>com.twitter.finagle.context.LocalContext.let(LocalContext.scala:28)</element>
- <element>com.twitter.finagle.http.exp.GenStreamingSerialServerDispatcher.$anonfun$dispatchAndHandleFn$1(GenStreamingSerialServerDispatcher.scala:83)</element>
- <element>com.twitter.util.Future.$anonfun$flatMap$1(Future.scala:1812)</element>
- <element>com.twitter.util.Promise$FutureTransformer.liftedTree1$1(Promise.scala:240)</element>
- <element>com.twitter.util.Promise$FutureTransformer.k(Promise.scala:240)</element>
- <element>com.twitter.util.Promise$Transformer.apply(Promise.scala:215)</element>
- <element>com.twitter.util.Promise$WaitQueue.com$twitter$util$Promise$WaitQueue$$run(Promise.scala:91)</element>
- <element>com.twitter.util.Promise$WaitQueue$$anon$1.run(Promise.scala:86)</element>
- <element>com.twitter.concurrent.LocalScheduler$Activation.run(Scheduler.scala:167)</element>
- <element>com.twitter.concurrent.LocalScheduler$Activation.submit(Scheduler.scala:126)</element>
- <element>com.twitter.concurrent.LocalScheduler.submit(Scheduler.scala:243)</element>
- <element>com.twitter.concurrent.Scheduler$.submit(Scheduler.scala:78)</element>
- <element>com.twitter.util.Promise$WaitQueue.runInScheduler(Promise.scala:86)</element>
- <element>com.twitter.util.Promise.updateIfEmpty(Promise.scala:783)</element>
- <element>com.twitter.util.Promise.update(Promise.scala:755)</element>
- <element>com.twitter.util.Promise.setValue(Promise.scala:731)</element>
- <element>com.twitter.concurrent.AsyncQueue.offer(AsyncQueue.scala:123)</element>
- <element>com.twitter.finagle.netty4.transport.ChannelTransport$$anon$2.channelRead(ChannelTransport.scala:169)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element>
- <element>com.twitter.finagle.netty4.http.handler.UnpoolHttpHandler$.channelRead(UnpoolHttpHandler.scala:32)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element>
- <element>com.twitter.finagle.netty4.http.handler.BadRequestHandler.channelRead(BadRequestHandler.scala:42)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element>
- <element>com.twitter.finagle.netty4.http.handler.HeaderValidatorHandler$.channelRead(HeaderValidatorHandler.scala:51)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element>
- <element>com.twitter.finagle.netty4.http.handler.UriValidatorHandler$.channelRead(UriValidatorHandler.scala:29)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element>
- <element>io.netty.handler.codec.MessageToMessageDecoder.channelRead(MessageToMessageDecoder.java:102)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element>
- <element>io.netty.handler.codec.MessageToMessageDecoder.channelRead(MessageToMessageDecoder.java:102)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element>
- <element>io.netty.handler.codec.MessageToMessageDecoder.channelRead(MessageToMessageDecoder.java:102)</element>
- <element>io.netty.handler.codec.MessageToMessageCodec.channelRead(MessageToMessageCodec.java:111)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element>
- <element>io.netty.channel.CombinedChannelDuplexHandler$DelegatingChannelHandlerContext.fireChannelRead(CombinedChannelDuplexHandler.java:436)</element>
- <element>io.netty.handler.codec.ByteToMessageDecoder.fireChannelRead(ByteToMessageDecoder.java:321)</element>
- <element>io.netty.handler.codec.ByteToMessageDecoder.channelRead(ByteToMessageDecoder.java:295)</element>
- <element>io.netty.channel.CombinedChannelDuplexHandler.channelRead(CombinedChannelDuplexHandler.java:251)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element>
- <element>io.netty.channel.DefaultChannelPipeline$HeadContext.channelRead(DefaultChannelPipeline.java:1410)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element>
- <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element>
- <element>io.netty.channel.DefaultChannelPipeline.fireChannelRead(DefaultChannelPipeline.java:919)</element>
- <element>io.netty.channel.nio.AbstractNioByteChannel$NioByteUnsafe.read(AbstractNioByteChannel.java:163)</element>
- <element>io.netty.channel.nio.NioEventLoop.processSelectedKey(NioEventLoop.java:714)</element>
- <element>io.netty.channel.nio.NioEventLoop.processSelectedKeysOptimized(NioEventLoop.java:650)</element>
- <element>io.netty.channel.nio.NioEventLoop.processSelectedKeys(NioEventLoop.java:576)</element>
- <element>io.netty.channel.nio.NioEventLoop.run(NioEventLoop.java:493)</element>
- <element>io.netty.util.concurrent.SingleThreadEventExecutor$4.run(SingleThreadEventExecutor.java:989)</element>
- <element>io.netty.util.internal.ThreadExecutorMap$2.run(ThreadExecutorMap.java:74)</element>
- <element>java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1130)</element>
- <element>java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:630)</element>
- <element>com.twitter.finagle.util.BlockingTimeTrackingThreadFactory$$anon$1.run(BlockingTimeTrackingThreadFactory.scala:23)</element>
- <element>io.netty.util.concurrent.FastThreadLocalRunnable.run(FastThreadLocalRunnable.java:30)</element>
- <element>java.base/java.lang.Thread.run(Thread.java:832)</element>
- </stacktrace>
-</error>
-
-</errors>
diff --git a/narration/IntegrationTests/SituationTheory.omdoc b/narration/IntegrationTests/SituationTheory.omdoc
index c94c552aa237aebd205e678bc900f0a8b313e46f..a0c67cd22db68986c003641b23a181471ac2bb72 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:1233.42.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="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#134.4.0:161.4.27"/></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:1087.44.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?SampleSituationTheory]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#194.6.0:221.6.27"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/MetaTheories.omdoc b/narration/MetaTheories.omdoc
index da33cd8937b732bf5a68014cecdd3a8eb11de736..f1014194a3bc36dcc4fee92df9d0289098c6a94a 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:804.26.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#358.14.0:453.14.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#455.15.0:475.15.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:888.30.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#442.18.0:537.18.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#539.19.0:559.19.20"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/Scrolls/TriangleScrolls.omdoc b/narration/Scrolls/TriangleScrolls.omdoc
index 73c6352cad919dafe6e33d904925a1e5722fcb70..068c49e7bac7999bcdfd1b22090ad10b185829a5 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:4188.123.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://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#79.4.0:273.13.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:4731.124.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><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#79.4.0:273.13.0"/></metadata>A blueprint problem theory for triangle scrolls
B
/|
/ |
@@ -7,6 +7,6 @@
/___|
A C
- (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#275.14.0:310.14.35"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#479.20.0:635.22.77"/></metadata>A blueprint problem theory for triangle scrolls that require a right angle
+ (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#275.14.0:310.14.35"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#579.20.0:735.22.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?TriangleScroll_RightAngledProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#637.23.0:676.23.39"/></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#846.31.0:860.31.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#1946.62.0:1963.62.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?Pythagoras]" target="http://mathhub.info/FrameIT/frameworld?Pythagoras"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#3037.93.0:3053.93.16"/></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?TriangleScroll_RightAngledProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#737.23.0:776.23.39"/></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#946.31.0:960.31.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#2046.62.0:2063.62.17"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/relational/Scrolls/TriangleScrolls.rel b/relational/Scrolls/TriangleScrolls.rel
index bb88c8a544673fb6c0186bd1a720dc6fdea674a1..fff48a866de028137e0f6abb13458d88f7de560f 100644
--- a/relational/Scrolls/TriangleScrolls.rel
+++ b/relational/Scrolls/TriangleScrolls.rel
@@ -3,4 +3,3 @@ Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc ht
Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem
Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?AngleSum
Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?OppositeLen
-Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?Pythagoras
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
index 3d24eaa36886067d93a355fe917c05f8b460eb68..f1cf578e33ff9de9b141901f54e2cb213f5eb2ec 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
@@ -60,4 +60,4 @@ DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angl
DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://cds.omdoc.org/urtheories?Strings?string?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel
index 034cb84689e96c78983a716213e30635d1c78d7b..98a5ed6ba63fd4f6af04ecf2a911081d8da3c0e9 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel
@@ -2,6 +2,7 @@ untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?label
untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?description
untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?problemTheory
untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?solutionTheory
+untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?label_verbalization_of
theory http://mathhub.info/FrameIT/frameworld?MetaAnnotations
HasMeta http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://cds.omdoc.org/urtheories?LF
Includes http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.info/MitM/Foundation?Strings
@@ -13,3 +14,5 @@ Declares http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.i
constant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?problemTheory
Declares http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.info/FrameIT/frameworld?MetaAnnotations?solutionTheory
constant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?solutionTheory
+Declares http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.info/FrameIT/frameworld?MetaAnnotations?label_verbalization_of
+constant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?label_verbalization_of
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
index dbb597819a2bf8fcd943925f4b8498be05539d2a..da2b8a6cf5bef00d2593566570fd4c196c7fedb2 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
@@ -58,4 +58,4 @@ DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solutio
DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://cds.omdoc.org/urtheories?Strings?string?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel
index 8bbadc7766d3e3191d5c23d86fd8efef814d0a2d..8c07a175d2b13c6cfa670a9ab73d466fa7b02d0c 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel
@@ -41,3 +41,28 @@ DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?
DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?addition?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?squareRoot?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?InformalProofs?trivial?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?exponentiation?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Strings?string?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel
index e902a2574ed7217562cfc8f556e1c1559e478c88..c90b58ee35f5188837199e705ddf2a13f4013a4d 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel
@@ -47,7 +47,7 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituatio
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?C?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://cds.omdoc.org/urtheories?Strings?string?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC
constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
@@ -73,7 +73,7 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituatio
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?A?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?B?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://cds.omdoc.org/urtheories?Strings?string?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC
constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
@@ -99,4 +99,4 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituatio
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?A?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?B?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://cds.omdoc.org/urtheories?Strings?string?type
diff --git a/source/IntegrationTests/SituationTheory.mmt b/source/IntegrationTests/SituationTheory.mmt
index a81ac7eca5abdd49f143232213f7f3fecb65f467..c8898d35c209bdf9217165480aab0278d2fe8c51 100644
--- a/source/IntegrationTests/SituationTheory.mmt
+++ b/source/IntegrationTests/SituationTheory.mmt
@@ -10,36 +10,36 @@ theory SampleSituationTheory =
A
: point â˜
= ⟨0.0, 0.0, 0.0⟩ â˜
- meta frameworld:?MetaAnnotations?label "Point A"
+ meta frameworld:?MetaAnnotations?label "A"
â™
B
: point â˜
= ⟨3.0, 3.0, 0.0⟩ â˜
- meta frameworld:?MetaAnnotations?label "Point B"
+ meta frameworld:?MetaAnnotations?label "B"
â™
C
: point â˜
= ⟨0.0, 3.0, 0.0⟩ â˜
- meta frameworld:?MetaAnnotations?label "Point C"
+ meta frameworld:?MetaAnnotations?label "C"
â™
distanceBC
: Σ x:â„. ⊦ (d- B C ≠x) â˜
= ⟨3.0, sketch "calculated by ComFreek by hand"⟩ â˜
- meta frameworld:?MetaAnnotations?label "distanceBC"
+ meta frameworld:?MetaAnnotations?label "BC"
â™
angleABC
: Σ β:â„. ⊦ ( ∠A,B,C ) ≠β â˜
= ⟨45.0, sketch "calculated by ComFreek by hand"⟩ â˜
- meta frameworld:?MetaAnnotations?label "distanceBC"
+ meta frameworld:?MetaAnnotations?label "∠ABC"
â™
angleBAC
: Σ β:â„. ⊦ ( ∠A,B,C ) ≠β â˜
= ⟨45.0, sketch "calculated by ComFreek by hand"⟩ â˜
- meta frameworld:?MetaAnnotations?label "distanceBC"
+ meta frameworld:?MetaAnnotations?label "∠BAC"
â™
âš
diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index 517507d63023dae6c9a39097e5312c0c6b47b494..cb2ec21951496c54043f153d85cf917ec98436c6 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -8,8 +8,12 @@ theory MetaAnnotations =
label â™
description â™
+
problemTheory â™
solutionTheoryâ™
+
+ /T example: lverb ?fact "default text" â™
+ label_verbalization_of # lverb â™
âš
/T The meta theory to use for situation theories, scroll problem, and scroll solution theories âš
diff --git a/source/Scrolls/TriangleScrolls.mmt b/source/Scrolls/TriangleScrolls.mmt
index 0d5bf5981de4aab8eafe258052c1e6fa647bad16..71f4c89681ee4ca8ccff471823f4a6b0371dbd68 100644
--- a/source/Scrolls/TriangleScrolls.mmt
+++ b/source/Scrolls/TriangleScrolls.mmt
@@ -13,9 +13,9 @@ fixmeta ?FrameworldMeta âš
(nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)
âš
theory TriangleScroll_GeneralProblem =
- A: point ☠meta ?MetaAnnotations?label "Point A"â™
- B: point ☠meta ?MetaAnnotations?label "Point B"â™
- C: point ☠meta ?MetaAnnotations?label "Point C"â™
+ A: point ☠meta ?MetaAnnotations?label lverb ?TriangleScroll_GeneralProblem?A "A" â™
+ B: point ☠meta ?MetaAnnotations?label lverb ?TriangleScroll_GeneralProblem?B "B"â™
+ C: point ☠meta ?MetaAnnotations?label lverb ?TriangleScroll_GeneralProblem?C "C"â™
âš
/T A blueprint problem theory for triangle scrolls that require a right angle
@@ -79,7 +79,7 @@ theory OppositeLen =
meta ?MetaAnnotations?label "OppositeLen" â™
meta ?MetaAnnotations?problemTheory ?OppositeLen/OppositeLen_Problem â™
meta ?MetaAnnotations?solutionTheory ?OppositeLen/OppositeLen_Solution â™
- meta ?MetaAnnotations?description "Given a triangle ABC right angled at C, the distance AB can be computed from the angle at B and the distance BC" â™
+ meta ?MetaAnnotations?description s"Given a triangle ${lverb ?TriangleScroll_GeneralProblem?A "A"}${lverb ?TriangleScroll_GeneralProblem?B "B"}${lverb ?TriangleScroll_GeneralProblem?C "C"} right angled at ${lverb ?TriangleScroll_GeneralProblem?C "C"}, the distance ${lverb ?TriangleScroll_GeneralProblem?A "A"}${lverb ?TriangleScroll_GeneralProblem?B "B"} can be computed from the angle at ${lverb ?TriangleScroll_GeneralProblem?B "B"} and the distance ${lverb ?TriangleScroll_GeneralProblem?B "B"}${lverb ?TriangleScroll_GeneralProblem?C "C"}" â™
include ?OppositeLen/OppositeLen_Problem â™
@@ -91,7 +91,8 @@ theory OppositeLen =
âš
âš
-theory Pythagoras =
+// Doesn't typecheck, not sure why âš
+// theory Pythagoras =
theory Pythagoras_Problem =
include ?TriangleScroll_RightAngledProblem â™
@@ -106,7 +107,7 @@ theory Pythagoras =
â™
âš
- theory Pythagoras_Solution =
+ // theory Pythagoras_Solution =
meta ?MetaAnnotations?label "Pythagoras" â™
meta ?MetaAnnotations?problemTheory ?Pythagoras/Pythagoras_Problem â™
meta ?MetaAnnotations?solutionTheory ?Pythagoras/Pythagoras_Solution â™
@@ -121,4 +122,4 @@ theory Pythagoras =
meta ?MetaAnnotations?description "Deduced length of hypotenuse AB"
â™
âš
-âš
\ No newline at end of file
+// âš
\ No newline at end of file