73 val string_of_typ_global: theory -> typ -> string |
73 val string_of_typ_global: theory -> typ -> string |
74 val string_of_sort_global: theory -> sort -> string |
74 val string_of_sort_global: theory -> sort -> string |
75 type syntax |
75 type syntax |
76 val eq_syntax: syntax * syntax -> bool |
76 val eq_syntax: syntax * syntax -> bool |
77 val force_syntax: syntax -> unit |
77 val force_syntax: syntax -> unit |
78 val get_infix: syntax -> string -> {assoc: Syntax_Ext.assoc, delim: string, pri: int} option |
78 val get_infix: syntax -> string -> {assoc: Printer.assoc, delim: string, pri: int} option |
79 val lookup_const: syntax -> string -> string option |
79 val lookup_const: syntax -> string -> string option |
80 val is_keyword: syntax -> string -> bool |
80 val is_keyword: syntax -> string -> bool |
81 val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list |
81 val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list |
82 val parse: syntax -> string -> Lexicon.token list -> Parser.parsetree list |
82 val parse: syntax -> string -> Lexicon.token list -> Parser.parsetree list |
83 val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option |
83 val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option |
417 |
417 |
418 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2; |
418 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2; |
419 |
419 |
420 fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram); |
420 fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram); |
421 |
421 |
422 fun get_infix (Syntax ({input, ...}, _)) c = Syntax_Ext.get_infix input c; |
422 fun get_infix (Syntax ({prtabs, ...}, _)) c = Printer.get_infix prtabs c; |
423 |
423 |
424 fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts; |
424 fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts; |
425 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode; |
425 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode; |
426 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; |
426 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; |
427 fun parse (Syntax ({gram, ...}, _)) = Parser.parse (Lazy.force gram); |
427 fun parse (Syntax ({gram, ...}, _)) = Parser.parse (Lazy.force gram); |