58 def name: Parser[String] = atom("name declaration", _.is_name) |
58 def name: Parser[String] = atom("name declaration", _.is_name) |
59 def xname: Parser[String] = atom("name reference", _.is_xname) |
59 def xname: Parser[String] = atom("name reference", _.is_xname) |
60 def text: Parser[String] = atom("text", _.is_text) |
60 def text: Parser[String] = atom("text", _.is_text) |
61 def ML_source: Parser[String] = atom("ML source", _.is_text) |
61 def ML_source: Parser[String] = atom("ML source", _.is_text) |
62 def doc_source: Parser[String] = atom("document source", _.is_text) |
62 def doc_source: Parser[String] = atom("document source", _.is_text) |
63 def path: Parser[String] = atom("file name/path specification", _.is_name) |
63 def path: Parser[String] = |
|
64 atom("file name/path specification", tok => tok.is_name && Path.is_ok(tok.content)) |
|
65 def theory_name: Parser[String] = |
|
66 atom("theory name", tok => tok.is_name && Thy_Load.is_ok(tok.content)) |
64 |
67 |
65 private def tag_name: Parser[String] = |
68 private def tag_name: Parser[String] = |
66 atom("tag name", tok => |
69 atom("tag name", tok => |
67 tok.kind == Token.Kind.IDENT || |
70 tok.kind == Token.Kind.IDENT || |
68 tok.kind == Token.Kind.STRING) |
71 tok.kind == Token.Kind.STRING) |