# HG changeset patch
# User wenzelm
# Date 780597299 -3600
# Node ID 2b1e384fae33e922eeca9bbf60c7eee301a888f1
# Parent  84ac5f101bd1e051c98d263a5058413c58dec8af
explode_tr now produces leadings 0s;
implode_ast_tr' now quotes result;

diff -r 84ac5f101bd1 -r 2b1e384fae33 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Wed Sep 21 15:39:02 1994 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Mon Sep 26 17:34:59 1994 +0100
@@ -116,7 +116,7 @@
   | bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
 
 
-(* explode atoms *)
+(* explode strings *)
 
 fun explode_tr (*"_explode"*) (ts as [consC, nilC, bit0, bit1, txt]) =
       let
@@ -127,8 +127,10 @@
           | encode_bit 1 = bit1
           | encode_bit _ = sys_error "encode_bit";
 
-        fun encode_char c =   (* FIXME leading 0s (?) *)
-          mk_list (map encode_bit (radixpand (2, (ord c))));
+        fun encode_char c =
+          let val bits = radixpand (2, ord c) in
+            mk_list (map encode_bit (replicate (8 - length bits) 0 @ bits))
+          end;
 
         val str =
           (case txt of
@@ -274,7 +276,7 @@
   | dependent_tr' _ _ = raise Match;
 
 
-(* implode atoms *)
+(* implode strings *)
 
 fun implode_ast_tr' (*"_implode"*) (asts as [Constant cons_name, nilC,
     bit0, bit1, bitss]) =
@@ -294,7 +296,7 @@
         fun decode_char bits =
           chr (#1 (scan_radixint (2, map decode_bit (strip_list bits))));
       in
-        Variable (implode (map decode_char (strip_list bitss)))
+        Variable ("''" ^ implode (map decode_char (strip_list bitss)) ^ "''")
       end
   | implode_ast_tr' (*"_implode"*) asts = raise_ast "implode_ast_tr'" asts;