tuned signature -- less cryptic ASCII names;
authorwenzelm
Tue Jul 12 15:32:16 2011 +0200 (2011-07-12)
changeset 4377722c87ff1b8a9
parent 43776 6dd13e111d30
child 43778 ce9189450447
tuned signature -- less cryptic ASCII names;
src/Pure/General/symbol.ML
src/Pure/General/yxml.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
     1.1 --- a/src/Pure/General/symbol.ML	Tue Jul 12 15:17:37 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.ML	Tue Jul 12 15:32:16 2011 +0200
     1.3 @@ -7,10 +7,7 @@
     1.4  signature SYMBOL =
     1.5  sig
     1.6    type symbol = string
     1.7 -  val SOH: symbol
     1.8    val STX: symbol
     1.9 -  val ENQ: symbol
    1.10 -  val ACK: symbol
    1.11    val DEL: symbol
    1.12    val space: symbol
    1.13    val spaces: int -> string
    1.14 @@ -89,10 +86,7 @@
    1.15  
    1.16  type symbol = string;
    1.17  
    1.18 -val SOH = chr 1;
    1.19  val STX = chr 2;
    1.20 -val ENQ = chr 5;
    1.21 -val ACK = chr 6;
    1.22  val DEL = chr 127;
    1.23  
    1.24  val space = chr 32;
     2.1 --- a/src/Pure/General/yxml.ML	Tue Jul 12 15:17:37 2011 +0200
     2.2 +++ b/src/Pure/General/yxml.ML	Tue Jul 12 15:32:16 2011 +0200
     2.3 @@ -15,6 +15,8 @@
     2.4  
     2.5  signature YXML =
     2.6  sig
     2.7 +  val X: Symbol.symbol
     2.8 +  val Y: Symbol.symbol
     2.9    val embed_controls: string -> string
    2.10    val detect: string -> bool
    2.11    val output_markup: Markup.T -> string * string
    2.12 @@ -45,8 +47,8 @@
    2.13  
    2.14  (* markers *)
    2.15  
    2.16 -val X = Symbol.ENQ;
    2.17 -val Y = Symbol.ACK;
    2.18 +val X = chr 5;
    2.19 +val Y = chr 6;
    2.20  val XY = X ^ Y;
    2.21  val XYX = XY ^ X;
    2.22  
     3.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 12 15:17:37 2011 +0200
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 12 15:32:16 2011 +0200
     3.3 @@ -22,7 +22,7 @@
     3.4  val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
     3.5  val test_markupN = "test_markup";          (*XML markup for everything*)
     3.6  
     3.7 -fun special ch = Symbol.SOH ^ ch;
     3.8 +fun special ch = chr 1 ^ ch;
     3.9  
    3.10  
    3.11  (* render markup *)