# HG changeset patch
# User wenzelm
# Date 977608219 -3600
# Node ID d4fda7d05ce51c948acec28408ae3637a5796d04
# Parent  f44ab310820216a9ed84d234ef91ddbe0de3d737
Tools/string_syntax.ML;

diff -r f44ab3108202 -r d4fda7d05ce5 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Dec 23 22:49:39 2000 +0100
+++ b/src/HOL/IsaMakefile	Sat Dec 23 22:50:19 2000 +0100
@@ -94,8 +94,8 @@
   Tools/datatype_package.ML Tools/datatype_prop.ML \
   Tools/datatype_rep_proofs.ML Tools/induct_attrib.ML Tools/induct_method.ML \
   Tools/inductive_package.ML Tools/meson.ML Tools/numeral_syntax.ML \
-  Tools/primrec_package.ML Tools/recdef_package.ML \
-  Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
+  Tools/primrec_package.ML Tools/recdef_package.ML Tools/record_package.ML \
+  Tools/string_syntax.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
   Transitive_Closure.ML Transitive_Closure.thy Wellfounded_Recursion.ML \
   Wellfounded_Recursion.thy Wellfounded_Relations.ML \
   Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
diff -r f44ab3108202 -r d4fda7d05ce5 src/HOL/String.thy
--- a/src/HOL/String.thy	Sat Dec 23 22:49:39 2000 +0100
+++ b/src/HOL/String.thy	Sat Dec 23 22:50:19 2000 +0100
@@ -1,90 +1,25 @@
 (*  Title:      HOL/String.thy
     ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Hex chars and strings.
 *)
 
-String = List +
-
-datatype
-  nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
-         | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
+theory String = List
+files "Tools/string_syntax.ML":
 
-datatype
-  char = Char nibble nibble
+datatype nibble =
+    H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
+  | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
 
-types
-  string = char list
+datatype char = Char nibble nibble
+types string = "char list"
 
 syntax
-  "_Char"       :: xstr => char       ("CHR _")
-  "_String"     :: xstr => string     ("_")
+  "_Char" :: "xstr => char"    ("CHR _")
+  "_String" :: "xstr => string"    ("_")
+
+setup StringSyntax.setup
 
 end
-
-
-ML
-
-local
-
-  (* chars *)
-
-  fun syntax_xstr x = Syntax.const "_xstr" $ Syntax.free x;
-
-
-  val zero = ord "0";
-  val ten = ord "A" - 10;
-
-  fun mk_nib n =
-    Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
-
-  fun dest_nib (Const (c, _)) =
-        (case explode c of
-          ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
-        | _ => raise Match)
-    | dest_nib _ = raise Match;
-
-  fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
-
-
-  fun mk_char c =
-    Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
-
-  fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
-    | dest_char _ = raise Match;
-
-
-  fun char_tr (*"_Char"*) [Free (xstr, _)] =
-        (case Syntax.explode_xstr xstr of
-          [c] => mk_char c
-        | _ => error ("Single character expected: " ^ xstr))
-    | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
-
-  fun char_tr' (*"Char"*) [t1, t2] =
-        Syntax.const "_Char" $ syntax_xstr (Syntax.implode_xstr [dest_nibs t1 t2])
-    | char_tr' (*"Char"*) _ = raise Match;
-
-
-  (* strings *)
-
-  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "Nil" $ Syntax.const "string"
-    | mk_string (t :: ts) = Syntax.const "Cons" $ t $ mk_string ts;
-
-  fun dest_string (Const ("Nil", _)) = []
-    | dest_string (Const ("Cons", _) $ c $ cs) = dest_char c :: dest_string cs
-    | dest_string _ = raise Match;
-
-
-  fun string_tr (*"_String"*) [Free (xstr, _)] =
-        mk_string (map mk_char (Syntax.explode_xstr xstr))
-    | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
-
-  fun cons_tr' (*"Cons"*) [c, cs] =
-        Syntax.const "_String" $
-          syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
-    | cons_tr' (*"Cons"*) ts = raise Match;
-
-in
-  val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
-  val print_translation = [("Char", char_tr'), ("Cons", cons_tr')];
-end;
diff -r f44ab3108202 -r d4fda7d05ce5 src/HOL/Tools/string_syntax.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/string_syntax.ML	Sat Dec 23 22:50:19 2000 +0100
@@ -0,0 +1,84 @@
+(*  Title:      HOL/Tools/string_syntax.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+Concrete syntax for hex chars and strings.  Assumes consts and syntax
+of theory HOL/String.
+*)
+
+signature STRING_SYNTAX =
+sig
+  val setup: (theory -> theory) list
+end;
+
+structure StringSyntax: STRING_SYNTAX =
+struct
+
+
+(* chars *)
+
+fun syntax_xstr x = Syntax.const "_xstr" $ Syntax.free x;
+
+
+val zero = ord "0";
+val ten = ord "A" - 10;
+
+fun mk_nib n =
+  Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
+
+fun dest_nib (Const (c, _)) =
+      (case explode c of
+        ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
+      | _ => raise Match)
+  | dest_nib _ = raise Match;
+
+fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
+
+
+fun mk_char c =
+  Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
+
+fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
+  | dest_char _ = raise Match;
+
+
+fun char_tr (*"_Char"*) [Free (xstr, _)] =
+      (case Syntax.explode_xstr xstr of
+        [c] => mk_char c
+      | _ => error ("Single character expected: " ^ xstr))
+  | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
+
+fun char_tr' (*"Char"*) [t1, t2] =
+      Syntax.const "_Char" $ syntax_xstr (Syntax.implode_xstr [dest_nibs t1 t2])
+  | char_tr' (*"Char"*) _ = raise Match;
+
+
+(* strings *)
+
+fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "Nil" $ Syntax.const "string"
+  | mk_string (t :: ts) = Syntax.const "Cons" $ t $ mk_string ts;
+
+fun dest_string (Const ("Nil", _)) = []
+  | dest_string (Const ("Cons", _) $ c $ cs) = dest_char c :: dest_string cs
+  | dest_string _ = raise Match;
+
+
+fun string_tr (*"_String"*) [Free (xstr, _)] =
+      mk_string (map mk_char (Syntax.explode_xstr xstr))
+  | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
+
+fun cons_tr' (*"Cons"*) [c, cs] =
+      Syntax.const "_String" $
+        syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
+  | cons_tr' (*"Cons"*) ts = raise Match;
+
+
+(* theory setup *)
+
+val setup =
+  [Theory.add_trfuns
+    ([], [("_Char", char_tr), ("_String", string_tr)],
+    [("Char", char_tr'), ("Cons", cons_tr')], [])];
+
+end;