clarified get_infix: avoid old ASCII input syntax;

--- a/src/Pure/Syntax/printer.ML	Wed Sep 26 13:36:10 2018 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed Sep 26 17:04:50 2018 +0200
@@ -28,6 +28,8 @@
   val show_type_emphasis: bool Config.T
   val type_emphasis: Proof.context -> typ -> bool
   type prtabs
+  datatype assoc = No_Assoc | Left_Assoc | Right_Assoc
+  val get_infix: prtabs -> string -> {assoc: assoc, delim: string, pri: int} 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
@@ -90,8 +92,30 @@
 
 type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
 
-fun mode_tab prtabs mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode);
-fun mode_tabs prtabs modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]);
+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 @ [""]);
+
+
+(* plain infix syntax *)
+
+datatype assoc = No_Assoc | Left_Assoc | Right_Assoc;
+
+fun is_space str = forall_string (fn s => s = " ") str;
+
+fun get_infix prtabs c =
+  Symtab.lookup_list (mode_tab prtabs "") c
+  |> map_filter (fn (symbs, _, p) =>
+      (case symbs of
+        [Block (_, [Arg p1, String (_, s), String (_, d), Break _, Arg p2])] =>
+          if is_space s andalso not (is_space d) then SOME (p1, p2, d, p) else NONE
+      | [Block (_, [TypArg p1, String (_, s), String (_, d), Break _, TypArg p2])] =>
+          if is_space s andalso not (is_space d) then SOME (p1, p2, d, p) else NONE
+      | _ => NONE))
+  |> get_first (fn (p1, p2, d, p) =>
+      if p1 = p + 1 andalso p2 = p + 1 then SOME {assoc = No_Assoc, delim = d, pri = p}
+      else if p1 = p andalso p2 = p + 1 then SOME {assoc = Left_Assoc, delim = d, pri = p}
+      else if p1 = p + 1 andalso p2 = p then SOME {assoc = Right_Assoc, delim = d, pri = p}
+      else NONE);
 
 
 (* xprod_to_fmt *)

--- a/src/Pure/Syntax/syntax.ML	Wed Sep 26 13:36:10 2018 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Sep 26 17:04:50 2018 +0200
@@ -75,7 +75,7 @@
   type syntax
   val eq_syntax: syntax * syntax -> bool
   val force_syntax: syntax -> unit
-  val get_infix: syntax -> string -> {assoc: Syntax_Ext.assoc, delim: string, pri: int} option
+  val get_infix: syntax -> string -> {assoc: Printer.assoc, delim: string, pri: int} 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 +419,7 @@
 
 fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram);
 
-fun get_infix (Syntax ({input, ...}, _)) c = Syntax_Ext.get_infix input c;
+fun get_infix (Syntax ({prtabs, ...}, _)) c = Printer.get_infix prtabs c;
 
 fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;

--- a/src/Pure/Syntax/syntax_ext.ML	Wed Sep 26 13:36:10 2018 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Wed Sep 26 17:04:50 2018 +0200
@@ -20,8 +20,6 @@
   datatype xprod = XProd of string * xsymb list * string * int
   val chain_pri: int
   val delims_of: xprod list -> string list list
-  datatype assoc = No_Assoc | Left_Assoc | Right_Assoc
-  val get_infix: xprod list -> string -> {assoc: assoc, delim: string, pri: int} option
   datatype syn_ext =
     Syn_Ext of {
       xprods: xprod list,
@@ -113,23 +111,6 @@
   |> map Symbol.explode;
 
 
-(* plain infix syntax *)
-
-datatype assoc = No_Assoc | Left_Assoc | Right_Assoc;
-
-fun get_infix xprods c =
-  xprods |> get_first (fn XProd (_, xsymbs, const, p) =>
-    if c = const then
-      (case xsymbs of
-        [Bg _, Argument (_, p1), Space _, Delim s, Brk _, Argument (_, p2), En] =>
-          if p1 = p + 1 andalso p2 = p + 1 then SOME {assoc = No_Assoc, delim = s, pri = p}
-          else if p1 = p andalso p2 = p + 1 then SOME {assoc = Left_Assoc, delim = s, pri = p}
-          else if p1 = p + 1 andalso p2 = p then SOME {assoc = Right_Assoc, delim = s, pri = p}
-          else NONE
-      | _ => NONE)
-    else NONE);
-
-
 
 (** datatype mfix **)
 

--- a/src/Pure/Thy/export_theory.ML	Wed Sep 26 13:36:10 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Wed Sep 26 17:04:50 2018 +0200
@@ -178,9 +178,9 @@
       let
         val ass =
           (case assoc of
-            Syntax_Ext.No_Assoc => 0
-          | Syntax_Ext.Left_Assoc => 1
-          | Syntax_Ext.Right_Assoc => 2);
+            Printer.No_Assoc => 0
+          | Printer.Left_Assoc => 1
+          | Printer.Right_Assoc => 2);
         open XML.Encode Term_XML.Encode;
       in triple int string int (ass, delim, pri) end;