# HG changeset patch
# User wenzelm
# Date 945890936 -3600
# Node ID ef78716f39ef67e7030a05034be261c0b24895ba
# Parent  93b62f856af7e44d4446cf636a45f6385c445fb8
text: string list;

diff -r 93b62f856af7 -r ef78716f39ef 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;