# HG changeset patch
# User wenzelm
# Date 1538162184 -7200
# Node ID 11529ae4578640dc7ea0295d04a5754c21b8e67e
# Parent  90cce2f79e77994c731efa977f91d9d9b6b80c03
more approximative prefix syntax, including binder;

diff -r 90cce2f79e77 -r 11529ae45786 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri Sep 28 19:30:07 2018 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri Sep 28 21:16:24 2018 +0200
@@ -30,6 +30,7 @@
   type prtabs
   datatype assoc = No_Assoc | Left_Assoc | Right_Assoc
   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,20 +97,35 @@
 fun mode_tabs (prtabs: prtabs) modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]);
 
 
-(* plain infix syntax *)
+(* approximative syntax *)
 
 datatype assoc = No_Assoc | Left_Assoc | Right_Assoc;
 
+local
+
+fun is_arg (Arg _) = true
+  | is_arg (TypArg _) = true
+  | is_arg _ = false;
+
 fun is_space str = forall_string (fn s => s = " ") str;
+val is_delim = not o is_space;
+
+fun is_delimiter (String (_, d)) = is_delim d
+  | is_delimiter _ = false;
+
+fun flatten (Block (_, symbs)) = maps flatten symbs
+  | flatten symb = [symb];
+
+in
 
 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
+          if is_space s andalso is_delim 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
+          if is_space s andalso is_delim 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}
@@ -117,6 +133,15 @@
       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;
+
 
 (* xprod_to_fmt *)
 
diff -r 90cce2f79e77 -r 11529ae45786 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;
diff -r 90cce2f79e77 -r 11529ae45786 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Sep 28 19:30:07 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Sep 28 21:16:24 2018 +0200
@@ -13,30 +13,35 @@
 structure Export_Theory: EXPORT_THEORY =
 struct
 
-(* infix syntax *)
+(* approximative syntax *)
 
-fun get_infix_type ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_type;
-fun get_infix_const ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_const;
-fun get_infix_fixed ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_fixed;
+val get_syntax = Syntax.get_approx o Proof_Context.syn_of;
+fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type;
+fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const;
+fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed;
 
-fun get_infix_param ctxt loc x =
+fun get_syntax_param ctxt loc x =
   let val thy = Proof_Context.theory_of ctxt in
     if Class.is_class thy loc then
       (case AList.lookup (op =) (Class.these_params thy [loc]) x of
         NONE => NONE
-      | SOME (_, (c, _)) => get_infix_const ctxt c)
-    else get_infix_fixed ctxt x
+      | SOME (_, (c, _)) => get_syntax_const ctxt c)
+    else get_syntax_fixed ctxt x
   end;
 
-fun encode_infix {assoc, delim, pri} =
-  let
-    val ass =
-      (case assoc of
-        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;
+val encode_syntax =
+  XML.Encode.variant
+   [fn NONE => ([], []),
+    fn SOME (Syntax.Prefix delim) => ([delim], []),
+    fn SOME (Syntax.Infix {assoc, delim, pri}) =>
+      let
+        val ass =
+          (case assoc of
+            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];
 
 
 (* standardization of variables: only frees and named bounds *)
@@ -102,7 +107,7 @@
   let
     val loc_ctxt = Locale.init loc thy;
     val args = Locale.params_of thy loc
-      |> map (fn ((x, T), _) => ((x, T), get_infix_param loc_ctxt loc x));
+      |> map (fn ((x, T), _) => ((x, T), get_syntax_param loc_ctxt loc x));
     val axioms =
       let
         val (intro1, intro2) = Locale.intros_of thy loc;
@@ -201,12 +206,12 @@
 
     val encode_type =
       let open XML.Encode Term_XML.Encode
-      in triple (option encode_infix) (list string) (option typ) end;
+      in triple encode_syntax (list string) (option typ) end;
 
     fun export_type c (Type.LogicalType n) =
-          SOME (encode_type (get_infix_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
+          SOME (encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
       | export_type c (Type.Abbreviation (args, U, false)) =
-          SOME (encode_type (get_infix_type thy_ctxt c, args, SOME U))
+          SOME (encode_type (get_syntax_type thy_ctxt c, args, SOME U))
       | export_type _ _ = NONE;
 
     val _ =
@@ -218,11 +223,11 @@
 
     val encode_const =
       let open XML.Encode Term_XML.Encode
-      in pair (option encode_infix) (pair (list string) (pair typ (option term))) end;
+      in pair encode_syntax (pair (list string) (pair typ (option term))) end;
 
     fun export_const c (T, abbrev) =
       let
-        val syntax = get_infix_const thy_ctxt c;
+        val syntax = get_syntax_const thy_ctxt c;
         val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
         val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
         val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
@@ -311,7 +316,7 @@
 
     fun encode_locale used =
       let open XML.Encode Term_XML.Encode in
-        triple (list (pair string sort)) (list (pair (pair string typ) (option encode_infix)))
+        triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax))
           (list (encode_axiom used))
       end;
 
diff -r 90cce2f79e77 -r 11529ae45786 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Fri Sep 28 19:30:07 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri Sep 28 21:16:24 2018 +0200
@@ -197,27 +197,32 @@
   }
 
 
-  /* infix syntax */
+  /* approximative syntax */
 
   object Assoc extends Enumeration
   {
     val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value
   }
 
-  sealed case class Infix(assoc: Assoc.Value, delim: String, pri: Int)
+  sealed abstract class Syntax
+  case object No_Syntax extends Syntax
+  case class Prefix(delim: String) extends Syntax
+  case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax
 
-  def decode_infix(body: XML.Body): Infix =
-  {
-    import XML.Decode._
-    val (ass, delim, pri) = triple(int, string, int)(body)
-    Infix(Assoc(ass), delim, pri)
-  }
+  def decode_syntax: XML.Decode.T[Syntax] =
+    XML.Decode.variant(List(
+      { case (Nil, Nil) => No_Syntax },
+      { case (List(delim), Nil) => Prefix(delim) },
+      { case (Nil, body) =>
+          import XML.Decode._
+          val (ass, delim, pri) = triple(int, string, int)(body)
+          Infix(Assoc(ass), delim, pri) }))
 
 
   /* types */
 
   sealed case class Type(
-    entity: Entity, syntax: Option[Infix], args: List[String], abbrev: Option[Term.Typ])
+    entity: Entity, syntax: Syntax, args: List[String], abbrev: Option[Term.Typ])
   {
     def cache(cache: Term.Cache): Type =
       Type(entity.cache(cache),
@@ -233,7 +238,7 @@
         val (syntax, args, abbrev) =
         {
           import XML.Decode._
-          triple(option(decode_infix), list(string), option(Term_XML.Decode.typ))(body)
+          triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body)
         }
         Type(entity, syntax, args, abbrev)
       })
@@ -243,7 +248,7 @@
 
   sealed case class Const(
     entity: Entity,
-    syntax: Option[Infix],
+    syntax: Syntax,
     typargs: List[String],
     typ: Term.Typ,
     abbrev: Option[Term.Term])
@@ -263,7 +268,7 @@
         val (syntax, (args, (typ, abbrev))) =
         {
           import XML.Decode._
-          pair(option(decode_infix), pair(list(string),
+          pair(decode_syntax, pair(list(string),
             pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))))(body)
         }
         Const(entity, syntax, args, typ, abbrev)
@@ -362,7 +367,7 @@
   sealed case class Locale(
     entity: Entity,
     typargs: List[(String, Term.Sort)],
-    args: List[((String, Term.Typ), Option[Infix])],
+    args: List[((String, Term.Typ), Syntax)],
     axioms: List[Prop])
   {
     def cache(cache: Term.Cache): Locale =
@@ -380,7 +385,7 @@
         {
           import XML.Decode._
           import Term_XML.Decode._
-          triple(list(pair(string, sort)), list(pair(pair(string, typ), option(decode_infix))),
+          triple(list(pair(string, sort)), list(pair(pair(string, typ), decode_syntax)),
             list(decode_prop))(body)
         }
         Locale(entity, typargs, args, axioms)