src/Pure/Isar/outer_syntax.scala
changeset 59702 58dfaa369c11
parent 59700 d887abcc7c24
child 59735 24bee1b11fce
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sun Mar 15 14:46:01 2015 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sun Mar 15 19:21:15 2015 +0100
     1.3 @@ -123,7 +123,9 @@
     1.4      }
     1.5  
     1.6  
     1.7 -  /* load commands */
     1.8 +  /* command categories */
     1.9 +
    1.10 +  def is_theory_begin(name: String): Boolean = keywords.is_command_kind(name, Keyword.theory_begin)
    1.11  
    1.12    def load_command(name: String): Option[List[String]] = keywords.load_command(name)
    1.13    def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
    1.14 @@ -284,7 +286,7 @@
    1.15      /* result structure */
    1.16  
    1.17      val spans = parse_spans(text)
    1.18 -    spans.foreach(span => add(Command(Document_ID.none, node_name, None, span)))
    1.19 +    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
    1.20      result()
    1.21    }
    1.22  }