text: string list;
authorwenzelm
Wed, 22 Dec 1999 20:28:56 +0100
changeset 8076 ef78716f39ef
parent 8075 93b62f856af7
child 8077 5c7b133fd26f
text: string list;
src/Pure/Isar/comment.ML
--- a/src/Pure/Isar/comment.ML	Wed Dec 22 17:20:01 1999 +0100
+++ b/src/Pure/Isar/comment.ML	Wed Dec 22 20:28:56 1999 +0100
@@ -9,7 +9,7 @@
 sig
   type text
   val string_of: text -> string
-  val plain: string -> text
+  val plain: string list -> text
   val none: text
   val ignore: 'a * text -> 'a
   type interest
@@ -25,11 +25,11 @@
 
 (** text **)
 
-datatype text = Text of string;
+datatype text = Text of string list;
 
-fun string_of (Text s) = s;
+fun string_of (Text ss) = cat_lines ss;
 val plain = Text;
-val none = plain "";
+val none = plain [];
 
 fun ignore (x, _) = x;