# HG changeset patch
# User wenzelm
# Date 1538166800 -7200
# Node ID a5e904112ea9eed892479e6ef5755fb4d4db9527
# Parent  11529ae4578640dc7ea0295d04a5754c21b8e67e
more accurate syntax: e.g. avoid brackets as prefix notation;

diff -r 11529ae45786 -r a5e904112ea9 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri Sep 28 21:16:24 2018 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri Sep 28 22:33:20 2018 +0200
@@ -29,8 +29,9 @@
   val type_emphasis: Proof.context -> typ -> bool
   type prtabs
   datatype assoc = No_Assoc | Left_Assoc | Right_Assoc
+  val get_prefix: prtabs -> Symtab.key -> string option
+  val get_binder: prtabs -> Symtab.key -> string option
   val get_infix: prtabs -> string -> {assoc: assoc, delim: string, pri: int} option
-  val get_prefix: prtabs -> Symtab.key -> string option
   val empty_prtabs: prtabs
   val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
   val remove_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
@@ -96,6 +97,8 @@
 fun mode_tab (prtabs: prtabs) mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode);
 fun mode_tabs (prtabs: prtabs) modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]);
 
+fun lookup_default prtabs = Symtab.lookup_list (mode_tab prtabs "");
+
 
 (* approximative syntax *)
 
@@ -118,8 +121,22 @@
 
 in
 
+fun get_prefix prtabs c =
+  lookup_default prtabs c
+  |> get_first (fn (symbs, _, _) =>
+      (case filter (is_arg orf is_delimiter) (maps flatten symbs) of
+        String (_, d) :: rest => if forall is_arg rest then SOME d else NONE
+      | _ => NONE));
+
+fun get_binder prtabs c =
+  lookup_default prtabs (Mixfix.binder_name c)
+  |> get_first (fn (symbs, _, _) =>
+      (case maps flatten symbs of
+        String (_, d) :: _ => if is_delim d then SOME d else NONE
+      | _ => NONE));
+
 fun get_infix prtabs c =
-  Symtab.lookup_list (mode_tab prtabs "") c
+  lookup_default prtabs c
   |> map_filter (fn (symbs, _, p) =>
       (case symbs of
         [Block (_, [Arg p1, String (_, s), String (_, d), Break _, Arg p2])] =>
@@ -133,13 +150,6 @@
       else if p1 = p + 1 andalso p2 = p then SOME {assoc = Right_Assoc, delim = d, pri = p}
       else NONE);
 
-fun get_prefix prtabs c =
-  Symtab.lookup_list (mode_tab prtabs "") c
-  |> get_first (fn (symbs, _, _) =>
-      (case filter (is_arg orf is_delimiter) (maps flatten symbs) of
-        String (_, d) :: _ => SOME d
-      | _ => NONE));
-
 end;
 
 
diff -r 11529ae45786 -r a5e904112ea9 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Sep 28 21:16:24 2018 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Sep 28 22:33:20 2018 +0200
@@ -427,7 +427,7 @@
   | NONE =>
       (case Printer.get_prefix prtabs c of
         SOME prfx => SOME prfx
-      | NONE => Printer.get_prefix prtabs (Mixfix.binder_name c))
+      | NONE => Printer.get_binder prtabs c)
       |> Option.map Prefix);
 
 fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;