# HG changeset patch
# User wenzelm
# Date 925488282 -7200
# Node ID 90fa592f6e6ea2dad7ce318b01228fe8fa4f78b8
# Parent  9b108dd75c2515ebda719b077b3c1603440950cd
added Isar/comment.ML;

diff -r 9b108dd75c25 -r 90fa592f6e6e src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Apr 30 18:02:16 1999 +0200
+++ b/src/Pure/IsaMakefile	Fri Apr 30 18:04:42 1999 +0200
@@ -28,8 +28,8 @@
   General/object.ML General/path.ML General/position.ML \
   General/pretty.ML General/scan.ML General/seq.ML General/source.ML \
   General/symbol.ML General/table.ML Isar/ROOT.ML Isar/args.ML \
-  Isar/attrib.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
-  Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
+  Isar/attrib.ML Isar/comment.ML Isar/isar.ML Isar/isar_cmd.ML \
+  Isar/isar_syn.ML Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
   Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \
   Isar/proof_context.ML Isar/proof_data.ML Isar/proof_history.ML \
   Isar/session.ML Isar/toplevel.ML ML-Systems/mlworks.ML \
diff -r 9b108dd75c25 -r 90fa592f6e6e src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Fri Apr 30 18:02:16 1999 +0200
+++ b/src/Pure/Isar/ROOT.ML	Fri Apr 30 18:04:42 1999 +0200
@@ -15,6 +15,7 @@
 use "method.ML";
 
 (*outer syntax*)
+use "comment.ML";
 use "outer_lex.ML";
 use "outer_parse.ML";
 
diff -r 9b108dd75c25 -r 90fa592f6e6e src/Pure/Isar/comment.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/comment.ML	Fri Apr 30 18:04:42 1999 +0200
@@ -0,0 +1,34 @@
+(*  Title:      Pure/Isar/comment.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Formal comments.
+*)
+
+signature COMMENT =
+sig
+  type text
+  val plain: string -> text
+  val empty: text
+  type interest
+  val no_interest: interest
+  val default_interest: interest
+end;
+
+structure Comment: COMMENT =
+struct
+
+(** text **)
+
+datatype text = Text of string;
+val plain = Text;
+val empty = plain "";
+
+
+(** interest **)
+
+datatype interest = Interest of bool;
+val no_interest = Interest false;
+val default_interest = Interest true;
+
+end;