--- a/src/Pure/Isar/document_structure.scala Wed Aug 10 18:57:20 2016 +0200
+++ b/src/Pure/Isar/document_structure.scala Thu Aug 11 15:32:53 2016 +0200
@@ -190,10 +190,15 @@
toks.filterNot(_.is_space) match {
case List(tok) if tok.is_comment =>
val s = tok.source
- if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
- else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
- else if (s.startsWith("(** ") && s.endsWith(" **)")) Some(2)
- else if (s.startsWith("(* ") && s.endsWith(" *)")) Some(3)
+ if (Word.codepoint_iterator(s).exists(c =>
+ Character.isLetter(c) || Character.isDigit(c)))
+ {
+ if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
+ else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
+ else if (s.startsWith("(** ") && s.endsWith(" **)")) Some(2)
+ else if (s.startsWith("(* ") && s.endsWith(" *)")) Some(3)
+ else None
+ }
else None
case _ => None
}