# HG changeset patch # User haftmann # Date 1191049135 -7200 # Node ID 95a315591af8e72f593698332f9f8e81e6bbf63a # Parent 151b3758f5765c63246d3aaefb68458d7cfe6917 added ocaml strings diff -r 151b3758f576 -r 95a315591af8 src/HOL/Library/ML_String.thy --- a/src/HOL/Library/ML_String.thy Sat Sep 29 08:58:54 2007 +0200 +++ b/src/HOL/Library/ML_String.thy Sat Sep 29 08:58:55 2007 +0200 @@ -47,6 +47,7 @@ code_type ml_string (SML "string") + (OCaml "string") (Haskell "String") setup {* @@ -63,6 +64,8 @@ in CodeTarget.add_pretty_ml_string "SML" charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR} + #> CodeTarget.add_pretty_ml_string "OCaml" + charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR} end *} @@ -70,12 +73,14 @@ (Haskell "_") code_reserved SML string +code_reserved OCaml string code_instance ml_string :: eq (Haskell -) code_const "op = \ ml_string \ ml_string \ bool" (SML "!((_ : string) = _)") + (OCaml "!((_ : string) = _)") (Haskell infixl 4 "==") end diff -r 151b3758f576 -r 95a315591af8 src/Tools/code/code_target.ML --- a/src/Tools/code/code_target.ML Sat Sep 29 08:58:54 2007 +0200 +++ b/src/Tools/code/code_target.ML Sat Sep 29 08:58:55 2007 +0200 @@ -1640,7 +1640,7 @@ ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char, pretty_string = ML_Syntax.print_string, pretty_numeral = fn unbounded => fn k => - if unbounded then "(" ^ string_of_int k ^ " : int)" + if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)" else string_of_int k, pretty_list = Pretty.enum "," "[" "]", infix_cons = (7, "::")}), @@ -1650,7 +1650,7 @@ then prefix "\\" (string_of_int i) else c end), - pretty_string = (fn _ => error "OCaml: no pretty strings"), + pretty_string = ML_Syntax.print_string, pretty_numeral = fn unbounded => fn k => if k >= 0 then if unbounded then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"