added Isar/comment.ML;
authorwenzelm
Fri Apr 30 18:04:42 1999 +0200 (1999-04-30)
changeset 654990fa592f6e6e
parent 6548 9b108dd75c25
child 6550 68f950b1a664
added Isar/comment.ML;
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/comment.ML
     1.1 --- a/src/Pure/IsaMakefile	Fri Apr 30 18:02:16 1999 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Fri Apr 30 18:04:42 1999 +0200
     1.3 @@ -28,8 +28,8 @@
     1.4    General/object.ML General/path.ML General/position.ML \
     1.5    General/pretty.ML General/scan.ML General/seq.ML General/source.ML \
     1.6    General/symbol.ML General/table.ML Isar/ROOT.ML Isar/args.ML \
     1.7 -  Isar/attrib.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
     1.8 -  Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
     1.9 +  Isar/attrib.ML Isar/comment.ML Isar/isar.ML Isar/isar_cmd.ML \
    1.10 +  Isar/isar_syn.ML Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
    1.11    Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \
    1.12    Isar/proof_context.ML Isar/proof_data.ML Isar/proof_history.ML \
    1.13    Isar/session.ML Isar/toplevel.ML ML-Systems/mlworks.ML \
     2.1 --- a/src/Pure/Isar/ROOT.ML	Fri Apr 30 18:02:16 1999 +0200
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Fri Apr 30 18:04:42 1999 +0200
     2.3 @@ -15,6 +15,7 @@
     2.4  use "method.ML";
     2.5  
     2.6  (*outer syntax*)
     2.7 +use "comment.ML";
     2.8  use "outer_lex.ML";
     2.9  use "outer_parse.ML";
    2.10  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/comment.ML	Fri Apr 30 18:04:42 1999 +0200
     3.3 @@ -0,0 +1,34 @@
     3.4 +(*  Title:      Pure/Isar/comment.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Markus Wenzel, TU Muenchen
     3.7 +
     3.8 +Formal comments.
     3.9 +*)
    3.10 +
    3.11 +signature COMMENT =
    3.12 +sig
    3.13 +  type text
    3.14 +  val plain: string -> text
    3.15 +  val empty: text
    3.16 +  type interest
    3.17 +  val no_interest: interest
    3.18 +  val default_interest: interest
    3.19 +end;
    3.20 +
    3.21 +structure Comment: COMMENT =
    3.22 +struct
    3.23 +
    3.24 +(** text **)
    3.25 +
    3.26 +datatype text = Text of string;
    3.27 +val plain = Text;
    3.28 +val empty = plain "";
    3.29 +
    3.30 +
    3.31 +(** interest **)
    3.32 +
    3.33 +datatype interest = Interest of bool;
    3.34 +val no_interest = Interest false;
    3.35 +val default_interest = Interest true;
    3.36 +
    3.37 +end;