97 val string_of_term_global: theory -> term -> string |
97 val string_of_term_global: theory -> term -> string |
98 val string_of_typ_global: theory -> typ -> string |
98 val string_of_typ_global: theory -> typ -> string |
99 val string_of_sort_global: theory -> sort -> string |
99 val string_of_sort_global: theory -> sort -> string |
100 type syntax |
100 type syntax |
101 val eq_syntax: syntax * syntax -> bool |
101 val eq_syntax: syntax * syntax -> bool |
|
102 val join_syntax: syntax -> unit |
102 val lookup_const: syntax -> string -> string option |
103 val lookup_const: syntax -> string -> string option |
103 val is_keyword: syntax -> string -> bool |
104 val is_keyword: syntax -> string -> bool |
104 val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list |
105 val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list |
105 val parse: Proof.context -> syntax -> string -> Lexicon.token list -> Parser.parsetree list |
106 val parse: Proof.context -> syntax -> string -> Lexicon.token list -> Parser.parsetree list |
106 val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option |
107 val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option |
506 print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table, |
507 print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table, |
507 prtabs: Printer.prtabs} * stamp; |
508 prtabs: Printer.prtabs} * stamp; |
508 |
509 |
509 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2; |
510 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2; |
510 |
511 |
|
512 fun join_syntax (Syntax ({gram, ...}, _)) = ignore (Future.join gram); |
|
513 |
511 fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts; |
514 fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts; |
512 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode; |
515 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode; |
513 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; |
516 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; |
514 fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt (Future.join gram); |
517 fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt (Future.join gram); |
515 |
518 |