# HG changeset patch
# User wenzelm
# Date 1537130734 -7200
# Node ID a015f1d3ba0c5fb466fb19136153ce2f10b9f1b7
# Parent  f0d4b1db0ea0712e0cb3b050a8257bf278908cca
export plain infix syntax;

diff -r f0d4b1db0ea0 -r a015f1d3ba0c src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Sep 16 20:33:37 2018 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Sep 16 22:45:34 2018 +0200
@@ -75,6 +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 lookup_const: syntax -> string -> string option
   val is_keyword: syntax -> string -> bool
   val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
@@ -418,6 +419,8 @@
 
 fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram);
 
+fun get_infix (Syntax ({input, ...}, _)) c = Syntax_Ext.get_infix input c;
+
 fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
diff -r f0d4b1db0ea0 -r a015f1d3ba0c src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Sun Sep 16 20:33:37 2018 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Sun Sep 16 22:45:34 2018 +0200
@@ -20,6 +20,8 @@
   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,
@@ -111,6 +113,23 @@
   |> 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 **)
 
diff -r f0d4b1db0ea0 -r a015f1d3ba0c src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sun Sep 16 20:33:37 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sun Sep 16 22:45:34 2018 +0200
@@ -52,14 +52,14 @@
     val parents = Theory.parents_of thy;
     val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
 
-    val ctxt = Proof_Context.init_global thy;
+    val thy_ctxt = Proof_Context.init_global thy;
 
 
     (* entities *)
 
     fun entity_markup space name =
       let
-        val xname = Name_Space.extern_shortest ctxt space name;
+        val xname = Name_Space.extern_shortest thy_ctxt space name;
         val {serial, pos, ...} = Name_Space.the_entry space name;
         val props =
           Position.offset_properties_of (adjust_pos pos) @
@@ -86,35 +86,53 @@
       in if null elems then () else export_body thy export_name elems end;
 
 
+    (* infix syntax *)
+
+    fun get_infix_const ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_const;
+    fun get_infix_type ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_type;
+
+    fun encode_infix {assoc, delim, pri} =
+      let
+        val ass =
+          (case assoc of
+            Syntax_Ext.No_Assoc => 0
+          | Syntax_Ext.Left_Assoc => 1
+          | Syntax_Ext.Right_Assoc => 2);
+        open XML.Encode Term_XML.Encode;
+      in triple int string int (ass, delim, pri) end;
+
+
     (* types *)
 
     val encode_type =
       let open XML.Encode Term_XML.Encode
-      in pair (list string) (option typ) end;
+      in triple (option encode_infix) (list string) (option typ) end;
 
-    fun export_type (Type.LogicalType n) =
-          SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
-      | export_type (Type.Abbreviation (args, U, false)) =
-          SOME (encode_type (args, SOME U))
-      | export_type _ = NONE;
+    fun export_type c (Type.LogicalType n) =
+          SOME (encode_type (get_infix_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))
+      | export_type _ _ = NONE;
 
     val _ =
-      export_entities "types" (K export_type) Sign.type_space
+      export_entities "types" export_type Sign.type_space
         (Name_Space.dest_table (#types rep_tsig));
 
 
     (* consts *)
 
     val encode_const =
-      let open XML.Encode Term_XML.Encode
-      in triple (list string) typ (option (term o named_bounds)) end;
+      let open XML.Encode Term_XML.Encode in
+        pair (option encode_infix) (pair (list string) (pair typ (option (term o named_bounds))))
+      end;
 
     fun export_const c (T, abbrev) =
       let
+        val syntax = get_infix_const thy_ctxt c;
         val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
         val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
         val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
-      in SOME (encode_const (args, T', abbrev')) end;
+      in SOME (encode_const (syntax, (args, (T', abbrev')))) end;
 
     val _ =
       export_entities "consts" export_const Sign.const_space
diff -r f0d4b1db0ea0 -r a015f1d3ba0c src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun Sep 16 20:33:37 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sun Sep 16 22:45:34 2018 +0200
@@ -190,12 +190,31 @@
   }
 
 
+  /* infix syntax */
+
+  object Assoc extends Enumeration
+  {
+    val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value
+  }
+
+  sealed case class Infix(assoc: Assoc.Value, delim: String, pri: Int)
+
+  def decode_infix(body: XML.Body): Infix =
+  {
+    import XML.Decode._
+    val (ass, delim, pri) = triple(int, string, int)(body)
+    Infix(Assoc(ass), delim, pri)
+  }
+
+
   /* types */
 
-  sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
+  sealed case class Type(
+    entity: Entity, syntax: Option[Infix], args: List[String], abbrev: Option[Term.Typ])
   {
     def cache(cache: Term.Cache): Type =
       Type(entity.cache(cache),
+        syntax,
         args.map(cache.string(_)),
         abbrev.map(cache.typ(_)))
   }
@@ -204,22 +223,27 @@
     provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.TYPE, tree)
-        val (args, abbrev) =
+        val (syntax, args, abbrev) =
         {
           import XML.Decode._
-          pair(list(string), option(Term_XML.Decode.typ))(body)
+          triple(option(decode_infix), list(string), option(Term_XML.Decode.typ))(body)
         }
-        Type(entity, args, abbrev)
+        Type(entity, syntax, args, abbrev)
       })
 
 
   /* consts */
 
   sealed case class Const(
-    entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
+    entity: Entity,
+    syntax: Option[Infix],
+    typargs: List[String],
+    typ: Term.Typ,
+    abbrev: Option[Term.Term])
   {
     def cache(cache: Term.Cache): Const =
       Const(entity.cache(cache),
+        syntax,
         typargs.map(cache.string(_)),
         cache.typ(typ),
         abbrev.map(cache.term(_)))
@@ -229,12 +253,13 @@
     provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.CONST, tree)
-        val (args, typ, abbrev) =
+        val (syntax, (args, (typ, abbrev))) =
         {
           import XML.Decode._
-          triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
+          pair(option(decode_infix), pair(list(string),
+            pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))))(body)
         }
-        Const(entity, args, typ, abbrev)
+        Const(entity, syntax, args, typ, abbrev)
       })