src/Pure/Isar/outer_parse.ML
changeset 6553 dc962d157a63
parent 6511 11b07125422e
child 6558 120ff48e8618
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Fri Apr 30 18:06:49 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Fri Apr 30 18:07:19 1999 +0200
     1.3 @@ -35,7 +35,9 @@
     1.4    val name: token list -> bstring * token list
     1.5    val xname: token list -> xstring * token list
     1.6    val text: token list -> string * token list
     1.7 -  val comment: token list -> string * token list
     1.8 +  val comment: token list -> Comment.text * token list
     1.9 +  val marg_comment: token list -> Comment.text * token list
    1.10 +  val interest: token list -> Comment.interest * token list
    1.11    val sort: token list -> xsort * token list
    1.12    val arity: token list -> (xsort list * xsort) * token list
    1.13    val simple_arity: token list -> (xsort list * xclass) * token list
    1.14 @@ -148,8 +150,14 @@
    1.15  
    1.16  val name = group "name declaration" (short_ident || sym_ident || string);
    1.17  val xname = group "name reference" (short_ident || long_ident || sym_ident || string);
    1.18 -val text = group "text" (short_ident || long_ident || string || verbatim);
    1.19 -val comment = Scan.optional ($$$ "--" |-- text) "";
    1.20 +val text = group "text" (short_ident || long_ident || sym_ident || string || verbatim);
    1.21 +
    1.22 +
    1.23 +(* formal comments *)
    1.24 +
    1.25 +val comment = text >> Comment.plain;
    1.26 +val marg_comment = Scan.optional ($$$ "--" |-- comment) Comment.empty;
    1.27 +val interest = Scan.optional ($$$ "%" >> K Comment.no_interest) Comment.default_interest;
    1.28  
    1.29  
    1.30  (* sorts and arities *)
    1.31 @@ -167,7 +175,7 @@
    1.32  (* types *)
    1.33  
    1.34  val typ =
    1.35 -  group "type" (short_ident || long_ident || type_ident || type_var || string);
    1.36 +  group "type" (short_ident || long_ident || sym_ident || type_ident || type_var || string);
    1.37  
    1.38  val type_args =
    1.39    type_ident >> single ||
    1.40 @@ -207,7 +215,7 @@
    1.41  
    1.42  (* terms *)
    1.43  
    1.44 -val trm = short_ident || long_ident || term_var || text_var || string;
    1.45 +val trm = short_ident || long_ident || sym_ident || term_var || text_var || string;
    1.46  
    1.47  val term = group "term" trm;
    1.48  val prop = group "proposition" trm;
    1.49 @@ -270,7 +278,7 @@
    1.50  and meth1 x = (enum1 "," meth2 >> (fn [m] => m | ms => Method.Then ms)) x
    1.51  and meth0 x = (enum1 "|" meth1 >> (fn [m] => m | ms => Method.Orelse ms)) x;
    1.52  
    1.53 -val method = meth3;
    1.54 +val method = meth4;
    1.55  
    1.56  
    1.57  end;