search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 23 forks source link

meta statement on document level throws exception when checking #509

Open ComFreek opened 4 years ago

ComFreek commented 4 years ago

  1. Create a new MMT file (in an arbitrary archive):

    namespace https://example.com/frameit/document-meta-exception ❚

meta ?xxx?yyy "zzz" ❙

    See panoptikum file here.

  2. Typecheck that file, e.g. in IntelliJ using the MMT plugin

  3. You'll receive some exception:

    13:52   MMT Error: class java.util.NoSuchElementException: null
                scala.collection.LinearSeqOptimized.last(LinearSeqOptimized.scala:150)
                scala.collection.LinearSeqOptimized.last$(LinearSeqOptimized.scala:149)
                scala.collection.immutable.List.last(List.scala:89)
                info.kwarc.mmt.api.parser.ParsingUnit.$anonfun$getLevel$2(Parser.scala:25)
                scala.Option.getOrElse(Option.scala:189)
                info.kwarc.mmt.api.parser.ParsingUnit.getLevel(Parser.scala:25)
                info.kwarc.mmt.api.parser.NotationBasedParser.makeTerm(NotationBasedParser.scala:367)
                info.kwarc.mmt.api.parser.NotationBasedParser.$anonfun$apply$10(NotationBasedParser.scala:218)
                info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)
                info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)
                info.kwarc.mmt.api.parser.NotationBasedParser.logGroup(NotationBasedParser.scala:72)
                info.kwarc.mmt.api.parser.NotationBasedParser.apply(NotationBasedParser.scala:218)
                info.kwarc.mmt.api.parser.KeywordBasedParser.puCont(StructureParser.scala:184)
                info.kwarc.mmt.api.parser.KeywordBasedParser.readParsedObject(StructureParser.sc... (show balloon)

Note that the meta statement must be of that form, i.e. exactly involve ?xxx?yyy and involve two strings. Otherwise, I couldn't get the exception reproduced.