src/Pure/Syntax/syntax.ML

--- a/src/Pure/Syntax/syntax.ML	Fri Sep 28 19:30:07 2018 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Sep 28 21:16:24 2018 +0200
@@ -75,7 +75,8 @@
   type syntax
   val eq_syntax: syntax * syntax -> bool
   val force_syntax: syntax -> unit
-  val get_infix: syntax -> string -> {assoc: Printer.assoc, delim: string, pri: int} option
+  datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int}
+  val get_approx: syntax -> string -> approx option
   val lookup_const: syntax -> string -> string option
   val is_keyword: syntax -> string -> bool
   val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
@@ -419,7 +420,15 @@
 
 fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram);
 
-fun get_infix (Syntax ({prtabs, ...}, _)) c = Printer.get_infix prtabs c;
+datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int};
+fun get_approx (Syntax ({prtabs, ...}, _)) c =
+  (case Printer.get_infix prtabs c of
+    SOME infx => SOME (Infix infx)
+  | NONE =>
+      (case Printer.get_prefix prtabs c of
+        SOME prfx => SOME prfx
+      | NONE => Printer.get_prefix prtabs (Mixfix.binder_name c))
+      |> Option.map Prefix);
 
 fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;