src/Pure/Thy/export_theory.ML
changeset 69077 11529ae45786
parent 69076 90cce2f79e77
child 69083 6f8ae6ddc26b
     1.1 --- a/src/Pure/Thy/export_theory.ML	Fri Sep 28 19:30:07 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Fri Sep 28 21:16:24 2018 +0200
     1.3 @@ -13,30 +13,35 @@
     1.4  structure Export_Theory: EXPORT_THEORY =
     1.5  struct
     1.6  
     1.7 -(* infix syntax *)
     1.8 +(* approximative syntax *)
     1.9  
    1.10 -fun get_infix_type ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_type;
    1.11 -fun get_infix_const ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_const;
    1.12 -fun get_infix_fixed ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_fixed;
    1.13 +val get_syntax = Syntax.get_approx o Proof_Context.syn_of;
    1.14 +fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type;
    1.15 +fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const;
    1.16 +fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed;
    1.17  
    1.18 -fun get_infix_param ctxt loc x =
    1.19 +fun get_syntax_param ctxt loc x =
    1.20    let val thy = Proof_Context.theory_of ctxt in
    1.21      if Class.is_class thy loc then
    1.22        (case AList.lookup (op =) (Class.these_params thy [loc]) x of
    1.23          NONE => NONE
    1.24 -      | SOME (_, (c, _)) => get_infix_const ctxt c)
    1.25 -    else get_infix_fixed ctxt x
    1.26 +      | SOME (_, (c, _)) => get_syntax_const ctxt c)
    1.27 +    else get_syntax_fixed ctxt x
    1.28    end;
    1.29  
    1.30 -fun encode_infix {assoc, delim, pri} =
    1.31 -  let
    1.32 -    val ass =
    1.33 -      (case assoc of
    1.34 -        Printer.No_Assoc => 0
    1.35 -      | Printer.Left_Assoc => 1
    1.36 -      | Printer.Right_Assoc => 2);
    1.37 -    open XML.Encode Term_XML.Encode;
    1.38 -  in triple int string int (ass, delim, pri) end;
    1.39 +val encode_syntax =
    1.40 +  XML.Encode.variant
    1.41 +   [fn NONE => ([], []),
    1.42 +    fn SOME (Syntax.Prefix delim) => ([delim], []),
    1.43 +    fn SOME (Syntax.Infix {assoc, delim, pri}) =>
    1.44 +      let
    1.45 +        val ass =
    1.46 +          (case assoc of
    1.47 +            Printer.No_Assoc => 0
    1.48 +          | Printer.Left_Assoc => 1
    1.49 +          | Printer.Right_Assoc => 2);
    1.50 +        open XML.Encode Term_XML.Encode;
    1.51 +      in ([], triple int string int (ass, delim, pri)) end];
    1.52  
    1.53  
    1.54  (* standardization of variables: only frees and named bounds *)
    1.55 @@ -102,7 +107,7 @@
    1.56    let
    1.57      val loc_ctxt = Locale.init loc thy;
    1.58      val args = Locale.params_of thy loc
    1.59 -      |> map (fn ((x, T), _) => ((x, T), get_infix_param loc_ctxt loc x));
    1.60 +      |> map (fn ((x, T), _) => ((x, T), get_syntax_param loc_ctxt loc x));
    1.61      val axioms =
    1.62        let
    1.63          val (intro1, intro2) = Locale.intros_of thy loc;
    1.64 @@ -201,12 +206,12 @@
    1.65  
    1.66      val encode_type =
    1.67        let open XML.Encode Term_XML.Encode
    1.68 -      in triple (option encode_infix) (list string) (option typ) end;
    1.69 +      in triple encode_syntax (list string) (option typ) end;
    1.70  
    1.71      fun export_type c (Type.LogicalType n) =
    1.72 -          SOME (encode_type (get_infix_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
    1.73 +          SOME (encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
    1.74        | export_type c (Type.Abbreviation (args, U, false)) =
    1.75 -          SOME (encode_type (get_infix_type thy_ctxt c, args, SOME U))
    1.76 +          SOME (encode_type (get_syntax_type thy_ctxt c, args, SOME U))
    1.77        | export_type _ _ = NONE;
    1.78  
    1.79      val _ =
    1.80 @@ -218,11 +223,11 @@
    1.81  
    1.82      val encode_const =
    1.83        let open XML.Encode Term_XML.Encode
    1.84 -      in pair (option encode_infix) (pair (list string) (pair typ (option term))) end;
    1.85 +      in pair encode_syntax (pair (list string) (pair typ (option term))) end;
    1.86  
    1.87      fun export_const c (T, abbrev) =
    1.88        let
    1.89 -        val syntax = get_infix_const thy_ctxt c;
    1.90 +        val syntax = get_syntax_const thy_ctxt c;
    1.91          val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
    1.92          val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
    1.93          val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
    1.94 @@ -311,7 +316,7 @@
    1.95  
    1.96      fun encode_locale used =
    1.97        let open XML.Encode Term_XML.Encode in
    1.98 -        triple (list (pair string sort)) (list (pair (pair string typ) (option encode_infix)))
    1.99 +        triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax))
   1.100            (list (encode_axiom used))
   1.101        end;
   1.102