# HG changeset patch
# User wenzelm
# Date 961969712 -7200
# Node ID b1dc56410b63f52916fda78f9af46c6bafe482d4
# Parent  ca8c6793dca594489396cffadf322acba26f8117
exception OUTPUT_FAIL of (string * Position.T) * exn
  (*note: actually belongs to isar_output.ML*);

diff -r ca8c6793dca5 -r b1dc56410b63 src/Pure/Isar/comment.ML
--- a/src/Pure/Isar/comment.ML	Sun Jun 25 23:48:09 2000 +0200
+++ b/src/Pure/Isar/comment.ML	Sun Jun 25 23:48:32 2000 +0200
@@ -3,7 +3,7 @@
     Author:     Markus Wenzel, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Formal comments.
+Internal markup of formal comments -- mostly dummy.
 *)
 
 signature COMMENT =
@@ -19,12 +19,13 @@
   val default_interest: interest
   val ignore_interest: 'a * interest -> 'a
   val ignore_interest': interest * 'a -> 'a
+  exception OUTPUT_FAIL of (string * Position.T) * exn
 end;
 
 structure Comment: COMMENT =
 struct
 
-(** text **)
+(* text *)
 
 datatype text = Text of string list;
 
@@ -35,8 +36,7 @@
 fun ignore (x, _) = x;
 
 
-
-(** interest **)
+(* interest *)
 
 datatype interest = Interest of int;
 val interest = Interest;
@@ -47,4 +47,9 @@
 fun ignore_interest' (_, x) = x;
 
 
+(* output errors *)
+
+(*note: actually belongs to isar_output.ML*)
+exception OUTPUT_FAIL of (string * Position.T) * exn;
+
 end;