clarified get_infix: avoid old ASCII input syntax;
authorwenzelm
Wed Sep 26 17:04:50 2018 +0200 (12 months ago)
changeset 690713ef82592dc22
parent 69070 a74b09822d79
child 69072 337b8ce5ff8d
clarified get_infix: avoid old ASCII input syntax;
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_ext.ML
src/Pure/Thy/export_theory.ML
     1.1 --- a/src/Pure/Syntax/printer.ML	Wed Sep 26 13:36:10 2018 +0200
     1.2 +++ b/src/Pure/Syntax/printer.ML	Wed Sep 26 17:04:50 2018 +0200
     1.3 @@ -28,6 +28,8 @@
     1.4    val show_type_emphasis: bool Config.T
     1.5    val type_emphasis: Proof.context -> typ -> bool
     1.6    type prtabs
     1.7 +  datatype assoc = No_Assoc | Left_Assoc | Right_Assoc
     1.8 +  val get_infix: prtabs -> string -> {assoc: assoc, delim: string, pri: int} option
     1.9    val empty_prtabs: prtabs
    1.10    val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
    1.11    val remove_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
    1.12 @@ -90,8 +92,30 @@
    1.13  
    1.14  type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
    1.15  
    1.16 -fun mode_tab prtabs mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode);
    1.17 -fun mode_tabs prtabs modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]);
    1.18 +fun mode_tab (prtabs: prtabs) mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode);
    1.19 +fun mode_tabs (prtabs: prtabs) modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]);
    1.20 +
    1.21 +
    1.22 +(* plain infix syntax *)
    1.23 +
    1.24 +datatype assoc = No_Assoc | Left_Assoc | Right_Assoc;
    1.25 +
    1.26 +fun is_space str = forall_string (fn s => s = " ") str;
    1.27 +
    1.28 +fun get_infix prtabs c =
    1.29 +  Symtab.lookup_list (mode_tab prtabs "") c
    1.30 +  |> map_filter (fn (symbs, _, p) =>
    1.31 +      (case symbs of
    1.32 +        [Block (_, [Arg p1, String (_, s), String (_, d), Break _, Arg p2])] =>
    1.33 +          if is_space s andalso not (is_space d) then SOME (p1, p2, d, p) else NONE
    1.34 +      | [Block (_, [TypArg p1, String (_, s), String (_, d), Break _, TypArg p2])] =>
    1.35 +          if is_space s andalso not (is_space d) then SOME (p1, p2, d, p) else NONE
    1.36 +      | _ => NONE))
    1.37 +  |> get_first (fn (p1, p2, d, p) =>
    1.38 +      if p1 = p + 1 andalso p2 = p + 1 then SOME {assoc = No_Assoc, delim = d, pri = p}
    1.39 +      else if p1 = p andalso p2 = p + 1 then SOME {assoc = Left_Assoc, delim = d, pri = p}
    1.40 +      else if p1 = p + 1 andalso p2 = p then SOME {assoc = Right_Assoc, delim = d, pri = p}
    1.41 +      else NONE);
    1.42  
    1.43  
    1.44  (* xprod_to_fmt *)
     2.1 --- a/src/Pure/Syntax/syntax.ML	Wed Sep 26 13:36:10 2018 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Sep 26 17:04:50 2018 +0200
     2.3 @@ -75,7 +75,7 @@
     2.4    type syntax
     2.5    val eq_syntax: syntax * syntax -> bool
     2.6    val force_syntax: syntax -> unit
     2.7 -  val get_infix: syntax -> string -> {assoc: Syntax_Ext.assoc, delim: string, pri: int} option
     2.8 +  val get_infix: syntax -> string -> {assoc: Printer.assoc, delim: string, pri: int} option
     2.9    val lookup_const: syntax -> string -> string option
    2.10    val is_keyword: syntax -> string -> bool
    2.11    val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
    2.12 @@ -419,7 +419,7 @@
    2.13  
    2.14  fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram);
    2.15  
    2.16 -fun get_infix (Syntax ({input, ...}, _)) c = Syntax_Ext.get_infix input c;
    2.17 +fun get_infix (Syntax ({prtabs, ...}, _)) c = Printer.get_infix prtabs c;
    2.18  
    2.19  fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
    2.20  fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
     3.1 --- a/src/Pure/Syntax/syntax_ext.ML	Wed Sep 26 13:36:10 2018 +0200
     3.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Wed Sep 26 17:04:50 2018 +0200
     3.3 @@ -20,8 +20,6 @@
     3.4    datatype xprod = XProd of string * xsymb list * string * int
     3.5    val chain_pri: int
     3.6    val delims_of: xprod list -> string list list
     3.7 -  datatype assoc = No_Assoc | Left_Assoc | Right_Assoc
     3.8 -  val get_infix: xprod list -> string -> {assoc: assoc, delim: string, pri: int} option
     3.9    datatype syn_ext =
    3.10      Syn_Ext of {
    3.11        xprods: xprod list,
    3.12 @@ -113,23 +111,6 @@
    3.13    |> map Symbol.explode;
    3.14  
    3.15  
    3.16 -(* plain infix syntax *)
    3.17 -
    3.18 -datatype assoc = No_Assoc | Left_Assoc | Right_Assoc;
    3.19 -
    3.20 -fun get_infix xprods c =
    3.21 -  xprods |> get_first (fn XProd (_, xsymbs, const, p) =>
    3.22 -    if c = const then
    3.23 -      (case xsymbs of
    3.24 -        [Bg _, Argument (_, p1), Space _, Delim s, Brk _, Argument (_, p2), En] =>
    3.25 -          if p1 = p + 1 andalso p2 = p + 1 then SOME {assoc = No_Assoc, delim = s, pri = p}
    3.26 -          else if p1 = p andalso p2 = p + 1 then SOME {assoc = Left_Assoc, delim = s, pri = p}
    3.27 -          else if p1 = p + 1 andalso p2 = p then SOME {assoc = Right_Assoc, delim = s, pri = p}
    3.28 -          else NONE
    3.29 -      | _ => NONE)
    3.30 -    else NONE);
    3.31 -
    3.32 -
    3.33  
    3.34  (** datatype mfix **)
    3.35  
     4.1 --- a/src/Pure/Thy/export_theory.ML	Wed Sep 26 13:36:10 2018 +0200
     4.2 +++ b/src/Pure/Thy/export_theory.ML	Wed Sep 26 17:04:50 2018 +0200
     4.3 @@ -178,9 +178,9 @@
     4.4        let
     4.5          val ass =
     4.6            (case assoc of
     4.7 -            Syntax_Ext.No_Assoc => 0
     4.8 -          | Syntax_Ext.Left_Assoc => 1
     4.9 -          | Syntax_Ext.Right_Assoc => 2);
    4.10 +            Printer.No_Assoc => 0
    4.11 +          | Printer.Left_Assoc => 1
    4.12 +          | Printer.Right_Assoc => 2);
    4.13          open XML.Encode Term_XML.Encode;
    4.14        in triple int string int (ass, delim, pri) end;
    4.15