--- a/src/Pure/Isar/token.ML Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Isar/token.ML Sat Nov 01 15:01:41 2014 +0100
@@ -44,7 +44,6 @@
val is_name: T -> bool
val is_proper: T -> bool
val is_improper: T -> bool
- val is_semicolon: T -> bool
val is_comment: T -> bool
val is_begin_ignore: T -> bool
val is_end_ignore: T -> bool
@@ -233,9 +232,6 @@
val is_improper = not o is_proper;
-fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
- | is_semicolon _ = false;
-
fun is_comment (Token (_, (Comment, _), _)) = true
| is_comment _ = false;
@@ -341,18 +337,16 @@
fun print tok = Markup.markup (markup tok) (unparse tok);
fun text_of tok =
- if is_semicolon tok then ("terminator", "")
- else
- let
- val k = str_of_kind (kind_of tok);
- val m = markup tok;
- val s = unparse tok;
- in
- if s = "" then (k, "")
- else if size s < 40 andalso not (exists_string (fn c => c = "\n") s)
- then (k ^ " " ^ Markup.markup m s, "")
- else (k, Markup.markup m s)
- end;
+ let
+ val k = str_of_kind (kind_of tok);
+ val m = markup tok;
+ val s = unparse tok;
+ in
+ if s = "" then (k, "")
+ else if size s < 40 andalso not (exists_string (fn c => c = "\n") s)
+ then (k ^ " " ^ Markup.markup m s, "")
+ else (k, Markup.markup m s)
+ end;