src/Pure/Thy/export_theory.ML
changeset 69003 a015f1d3ba0c
parent 68997 4278947ba336
child 69019 a6ba77af6486
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun Sep 16 20:33:37 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun Sep 16 22:45:34 2018 +0200
     1.3 @@ -52,14 +52,14 @@
     1.4      val parents = Theory.parents_of thy;
     1.5      val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
     1.6  
     1.7 -    val ctxt = Proof_Context.init_global thy;
     1.8 +    val thy_ctxt = Proof_Context.init_global thy;
     1.9  
    1.10  
    1.11      (* entities *)
    1.12  
    1.13      fun entity_markup space name =
    1.14        let
    1.15 -        val xname = Name_Space.extern_shortest ctxt space name;
    1.16 +        val xname = Name_Space.extern_shortest thy_ctxt space name;
    1.17          val {serial, pos, ...} = Name_Space.the_entry space name;
    1.18          val props =
    1.19            Position.offset_properties_of (adjust_pos pos) @
    1.20 @@ -86,35 +86,53 @@
    1.21        in if null elems then () else export_body thy export_name elems end;
    1.22  
    1.23  
    1.24 +    (* infix syntax *)
    1.25 +
    1.26 +    fun get_infix_const ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_const;
    1.27 +    fun get_infix_type ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_type;
    1.28 +
    1.29 +    fun encode_infix {assoc, delim, pri} =
    1.30 +      let
    1.31 +        val ass =
    1.32 +          (case assoc of
    1.33 +            Syntax_Ext.No_Assoc => 0
    1.34 +          | Syntax_Ext.Left_Assoc => 1
    1.35 +          | Syntax_Ext.Right_Assoc => 2);
    1.36 +        open XML.Encode Term_XML.Encode;
    1.37 +      in triple int string int (ass, delim, pri) end;
    1.38 +
    1.39 +
    1.40      (* types *)
    1.41  
    1.42      val encode_type =
    1.43        let open XML.Encode Term_XML.Encode
    1.44 -      in pair (list string) (option typ) end;
    1.45 +      in triple (option encode_infix) (list string) (option typ) end;
    1.46  
    1.47 -    fun export_type (Type.LogicalType n) =
    1.48 -          SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
    1.49 -      | export_type (Type.Abbreviation (args, U, false)) =
    1.50 -          SOME (encode_type (args, SOME U))
    1.51 -      | export_type _ = NONE;
    1.52 +    fun export_type c (Type.LogicalType n) =
    1.53 +          SOME (encode_type (get_infix_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
    1.54 +      | export_type c (Type.Abbreviation (args, U, false)) =
    1.55 +          SOME (encode_type (get_infix_type thy_ctxt c, args, SOME U))
    1.56 +      | export_type _ _ = NONE;
    1.57  
    1.58      val _ =
    1.59 -      export_entities "types" (K export_type) Sign.type_space
    1.60 +      export_entities "types" export_type Sign.type_space
    1.61          (Name_Space.dest_table (#types rep_tsig));
    1.62  
    1.63  
    1.64      (* consts *)
    1.65  
    1.66      val encode_const =
    1.67 -      let open XML.Encode Term_XML.Encode
    1.68 -      in triple (list string) typ (option (term o named_bounds)) end;
    1.69 +      let open XML.Encode Term_XML.Encode in
    1.70 +        pair (option encode_infix) (pair (list string) (pair typ (option (term o named_bounds))))
    1.71 +      end;
    1.72  
    1.73      fun export_const c (T, abbrev) =
    1.74        let
    1.75 +        val syntax = get_infix_const thy_ctxt c;
    1.76          val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
    1.77          val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
    1.78          val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
    1.79 -      in SOME (encode_const (args, T', abbrev')) end;
    1.80 +      in SOME (encode_const (syntax, (args, (T', abbrev')))) end;
    1.81  
    1.82      val _ =
    1.83        export_entities "consts" export_const Sign.const_space