123 (*Note: the syntax for files is statically determined at the very |
123 (*Note: the syntax for files is statically determined at the very |
124 beginning; for interactive processing it may change dynamically.*) |
124 beginning; for interactive processing it may change dynamically.*) |
125 |
125 |
126 fun get_lexicons () = ! global_lexicons; |
126 fun get_lexicons () = ! global_lexicons; |
127 fun get_parsers () = ! global_parsers; |
127 fun get_parsers () = ! global_parsers; |
128 fun get_parser () = Option.map (#2 o #1) o Symtab.curried_lookup (get_parsers ()); |
128 fun get_parser () = Option.map (#2 o #1) o Symtab.lookup (get_parsers ()); |
129 |
129 |
130 fun command_tags name = |
130 fun command_tags name = |
131 (case Symtab.curried_lookup (get_parsers ()) name of |
131 (case Symtab.lookup (get_parsers ()) name of |
132 SOME (((_, k), _), _) => OuterKeyword.tags_of k |
132 SOME (((_, k), _), _) => OuterKeyword.tags_of k |
133 | NONE => []); |
133 | NONE => []); |
134 |
134 |
135 fun is_markup kind name = (AList.lookup (op =) (! global_markups) name = SOME kind); |
135 fun is_markup kind name = (AList.lookup (op =) (! global_markups) name = SOME kind); |
136 |
136 |
141 (Scan.extend_lexicon lex (map Symbol.explode keywords)))); |
141 (Scan.extend_lexicon lex (map Symbol.explode keywords)))); |
142 |
142 |
143 fun add_parser (Parser (name, (comment, kind, markup), int_only, parse)) tab = |
143 fun add_parser (Parser (name, (comment, kind, markup), int_only, parse)) tab = |
144 (if not (Symtab.defined tab name) then () |
144 (if not (Symtab.defined tab name) then () |
145 else warning ("Redefined outer syntax command " ^ quote name); |
145 else warning ("Redefined outer syntax command " ^ quote name); |
146 Symtab.curried_update (name, (((comment, kind), (int_only, parse)), markup)) tab); |
146 Symtab.update (name, (((comment, kind), (int_only, parse)), markup)) tab); |
147 |
147 |
148 fun add_parsers parsers = |
148 fun add_parsers parsers = |
149 (change_parsers (fold add_parser parsers); |
149 (change_parsers (fold add_parser parsers); |
150 change_lexicons (apsnd (fn lex => Scan.extend_lexicon lex |
150 change_lexicons (apsnd (fn lex => Scan.extend_lexicon lex |
151 (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers)))); |
151 (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers)))); |