src/Pure/Isar/token.ML

   val ident_with: (string -> bool) -> T -> bool
   val is_command: T -> bool
   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
   val is_error: T -> bool
   val is_space: T -> bool

   | is_proper (Token (_, (Comment, _), _)) = false
   | is_proper _ = true;
 
 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;
 
 fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
   | is_begin_ignore _ = false;

 fun unparse_src (Src {args, ...}) = map unparse args;
 
 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;
 
 
 
 (** associated values **)