equal
deleted
inserted
replaced
88 |
88 |
89 val scope = Parse.reserved "command" >> K Command || Parse.reserved "proof" >> K Proof; |
89 val scope = Parse.reserved "command" >> K Command || Parse.reserved "proof" >> K Proof; |
90 |
90 |
91 val tag_scope = |
91 val tag_scope = |
92 Parse.group (fn () => "document tag scope") (Parse.$$$ "(" |-- Parse.!!! (scope --| Parse.$$$ ")")); |
92 Parse.group (fn () => "document tag scope") (Parse.$$$ "(" |-- Parse.!!! (scope --| Parse.$$$ ")")); |
|
93 (*//---------------------------- test code: NO @{print} available ------------------------\\* ) |
|
94 fun tag_scope toks = |
|
95 let |
|
96 val xxx = |
|
97 (Parse.group (fn () => "document tag scope") |
|
98 (Parse.$$$ "(" |-- Parse.!!! (scope --| Parse.$$$ ")"))) toks |
|
99 val _ = @{print} {a = "Document_Source.tag_scope", result = xxx} |
|
100 in xxx end; |
|
101 ( *\\---------------------------- test code: NO @{print} available ------------------------//*) |
93 |
102 |
94 val tag_name = |
103 val tag_name = |
95 Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string); |
104 Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string); |
96 |
105 |
97 |
106 |