src/Pure/Syntax/syntax.ML
changeset 26678 a3ae088dc20f
parent 25993 d542486e39e7
child 26684 0701201def95
     1.1 --- a/src/Pure/Syntax/syntax.ML	Wed Apr 16 02:25:06 2008 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Apr 16 10:50:37 2008 +0200
     1.3 @@ -141,6 +141,7 @@
     1.4    val string_of_sort: Proof.context -> sort -> string
     1.5    val string_of_classrel: Proof.context -> class list -> string
     1.6    val string_of_arity: Proof.context -> arity -> string
     1.7 +  val guess_infix: syntax -> string -> mixfix option
     1.8    val pp: Proof.context -> Pretty.pp
     1.9  end;
    1.10  
    1.11 @@ -833,6 +834,13 @@
    1.12    fn x => pretty_classrel ctxt x,
    1.13    fn x => pretty_arity ctxt x);
    1.14  
    1.15 +(*educated guess for reconstructing infixes*)
    1.16 +fun guess_infix (Syntax (syn, _)) c = case Parser.guess_infix_lr (#gram syn) c
    1.17 + of SOME (s, l, r, j) => SOME (if l then Mixfix.InfixlName (s, j)
    1.18 +      else if r then Mixfix.InfixrName (s, j)
    1.19 +      else Mixfix.InfixName (s, j))
    1.20 +  | NONE => NONE
    1.21 +
    1.22  (*export parts of internal Syntax structures*)
    1.23  open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
    1.24