use simplified Syntax.escape;
authorwenzelm
Fri Feb 26 23:05:47 2010 +0100 (2010-02-26)
changeset 35390efad0e364738
parent 35389 2be5440f7271
child 35391 34d8e0a9bfa7
use simplified Syntax.escape;
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/Import/proof_kernel.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/syn_ext.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Feb 26 21:43:26 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Feb 26 23:05:47 2010 +0100
     1.3 @@ -49,25 +49,14 @@
     1.4    if line = 0 orelse col = 0 then no_label_name
     1.5    else label_prefix ^ string_of_int line ^ "_" ^ string_of_int col
     1.6  
     1.7 -local
     1.8 -  val quote_mixfix =
     1.9 -    Symbol.explode #> map
    1.10 -      (fn "_" => "'_"
    1.11 -        | "(" => "'("
    1.12 -        | ")" => "')"
    1.13 -        | "/" => "'/"
    1.14 -        | s => s) #>
    1.15 -    implode
    1.16 -in
    1.17  fun mk_syntax name i =
    1.18    let
    1.19 -    val syn = quote_mixfix name
    1.20 +    val syn = Syntax.escape name
    1.21      val args = concat (separate ",/ " (replicate i "_"))
    1.22    in
    1.23      if i = 0 then Mixfix (syn, [], 1000)
    1.24      else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000)
    1.25    end
    1.26 -end
    1.27  
    1.28  
    1.29  datatype attribute_value = StringValue of string | TermValue of term
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Feb 26 21:43:26 2010 +0100
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Feb 26 23:05:47 2010 +0100
     2.3 @@ -186,7 +186,7 @@
     2.4  
     2.5  fun mk_syn thy c =
     2.6    if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
     2.7 -  else Syntax.literal c
     2.8 +  else Delimfix (Syntax.escape c)
     2.9  
    2.10  fun quotename c =
    2.11    if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c
     3.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Feb 26 21:43:26 2010 +0100
     3.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Feb 26 23:05:47 2010 +0100
     3.3 @@ -21,7 +21,6 @@
     3.4  signature MIXFIX1 =
     3.5  sig
     3.6    include MIXFIX0
     3.7 -  val literal: string -> mixfix
     3.8    val no_syn: 'a * 'b -> 'a * 'b * mixfix
     3.9    val pretty_mixfix: mixfix -> Pretty.T
    3.10    val mixfix_args: mixfix -> int
    3.11 @@ -51,8 +50,6 @@
    3.12    Binder of string * int * int |
    3.13    Structure;
    3.14  
    3.15 -val literal = Delimfix o SynExt.escape_mfix;
    3.16 -
    3.17  fun no_syn (x, y) = (x, y, NoSyn);
    3.18  
    3.19  
     4.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Feb 26 21:43:26 2010 +0100
     4.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Feb 26 23:05:47 2010 +0100
     4.3 @@ -14,6 +14,7 @@
     4.4    val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
     4.5    val mk_trfun: string * 'a -> string * ('a * stamp)
     4.6    val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
     4.7 +  val escape: string -> string
     4.8    val tokentrans_mode:
     4.9      string -> (string * (Proof.context -> string -> Pretty.T)) list ->
    4.10      (string * string * (Proof.context -> string -> Pretty.T)) list
    4.11 @@ -54,7 +55,6 @@
    4.12        token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list}
    4.13    val mfix_delims: string -> string list
    4.14    val mfix_args: string -> int
    4.15 -  val escape_mfix: string -> string
    4.16    val syn_ext': bool -> (string -> bool) -> mfix list ->
    4.17      string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    4.18      (string * ((Proof.context -> term list -> term) * stamp)) list *
    4.19 @@ -229,7 +229,7 @@
    4.20  fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) [];
    4.21  val mfix_args = length o filter is_argument o read_mfix;
    4.22  
    4.23 -val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
    4.24 +val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
    4.25  
    4.26  end;
    4.27