# HG changeset patch
# User wenzelm
# Date 1013542417 -3600
# Node ID 21485940c8b966d637fcee6748856f2c9bf5d42b
# Parent  8e1cae1de136e87dcc879ebc43f6191efeeb55fe
eliminated Isar/comment.ML;

diff -r 8e1cae1de136 -r 21485940c8b9 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Feb 12 20:33:03 2002 +0100
+++ b/src/Pure/IsaMakefile	Tue Feb 12 20:33:37 2002 +0100
@@ -30,7 +30,7 @@
   General/source.ML General/symbol.ML General/table.ML General/url.ML	\
   General/xml.ML 		\
   Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML		\
-  Isar/auto_bind.ML Isar/calculation.ML Isar/comment.ML			\
+  Isar/auto_bind.ML Isar/calculation.ML          			\
   Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML		\
   Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML			\
   Isar/isar_thy.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML	\
diff -r 8e1cae1de136 -r 21485940c8b9 src/Pure/Isar/comment.ML
--- a/src/Pure/Isar/comment.ML	Tue Feb 12 20:33:03 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-(*  Title:      Pure/Isar/comment.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
-
-Internal markup of formal comments -- mostly dummy.
-*)
-
-signature COMMENT =
-sig
-  type text
-  val string_of: text -> string
-  val plain: string list -> text
-  val none: text
-  val ignore: 'a * text -> 'a
-  type interest
-  val interest: int -> interest
-  val no_interest: interest
-  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 *)
-
-datatype text = Text of string list;
-
-fun string_of (Text ss) = cat_lines ss;
-val plain = Text;
-val none = plain [];
-
-fun ignore (x, _) = x;
-
-
-(* interest *)
-
-datatype interest = Interest of int;
-val interest = Interest;
-val no_interest = interest ~1;
-val default_interest = interest 0;
-
-fun ignore_interest (x, _) = x;
-fun ignore_interest' (_, x) = x;
-
-
-(* output errors *)
-
-(*note: actually belongs to isar_output.ML*)
-exception OUTPUT_FAIL of (string * Position.T) * exn;
-
-end;