src/Pure/General/symbol.ML
changeset 29324 e07fc65e296b
parent 27903 af1b39debf30
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/General/symbol.ML	Fri Jan 02 22:42:08 2009 +0100
     1.2 +++ b/src/Pure/General/symbol.ML	Fri Jan 02 22:52:42 2009 +0100
     1.3 @@ -65,6 +65,7 @@
     1.4    val bump_string: string -> string
     1.5    val length: symbol list -> int
     1.6    val xsymbolsN: string
     1.7 +  val output: string -> output * int
     1.8  end;
     1.9  
    1.10  structure Symbol: SYMBOL =
    1.11 @@ -175,21 +176,22 @@
    1.12    ord space <= ord c andalso ord c <= ord "~" andalso c <> "." andalso c <> ">"
    1.13    orelse ord c >= 128;
    1.14  
    1.15 -fun encode_raw str =
    1.16 -  let
    1.17 -    val raw0 = enclose "\\<^raw:" ">";
    1.18 -    val raw1 = raw0 o implode;
    1.19 -    val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
    1.20 -
    1.21 -    fun encode cs = enc (Library.take_prefix raw_chr cs)
    1.22 -    and enc ([], []) = []
    1.23 -      | enc (cs, []) = [raw1 cs]
    1.24 -      | enc ([], d :: ds) = raw2 d :: encode ds
    1.25 -      | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;
    1.26 -  in
    1.27 -    if exists_string (not o raw_chr) str then implode (encode (explode str))
    1.28 -    else raw0 str
    1.29 -  end;
    1.30 +fun encode_raw "" = ""
    1.31 +  | encode_raw str =
    1.32 +      let
    1.33 +        val raw0 = enclose "\\<^raw:" ">";
    1.34 +        val raw1 = raw0 o implode;
    1.35 +        val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
    1.36 +    
    1.37 +        fun encode cs = enc (Library.take_prefix raw_chr cs)
    1.38 +        and enc ([], []) = []
    1.39 +          | enc (cs, []) = [raw1 cs]
    1.40 +          | enc ([], d :: ds) = raw2 d :: encode ds
    1.41 +          | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;
    1.42 +      in
    1.43 +        if exists_string (not o raw_chr) str then implode (encode (explode str))
    1.44 +        else raw0 str
    1.45 +      end;
    1.46  
    1.47  
    1.48  (* diagnostics *)
    1.49 @@ -519,9 +521,9 @@
    1.50  
    1.51  
    1.52  
    1.53 -(** xsymbols **)
    1.54 +(** symbol output **)
    1.55  
    1.56 -val xsymbolsN = "xsymbols";
    1.57 +(* length *)
    1.58  
    1.59  fun sym_len s =
    1.60    if not (is_printable s) then (0: int)
    1.61 @@ -532,8 +534,16 @@
    1.62  
    1.63  fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
    1.64  
    1.65 +
    1.66 +(* print mode *)
    1.67 +
    1.68 +val xsymbolsN = "xsymbols";
    1.69 +
    1.70 +fun output s = (s, sym_length (sym_explode s));
    1.71 +
    1.72 +
    1.73  (*final declarations of this structure!*)
    1.74 +val explode = sym_explode;
    1.75  val length = sym_length;
    1.76 -val explode = sym_explode;
    1.77  
    1.78  end;