# HG changeset patch
# User wenzelm
# Date 1470922373 -7200
# Node ID ff6caffcaed46481a1c0b1c763cd2e44d4054dcd
# Parent  5cdcd51a4dadf1c21abfece124bf07cf84efcaf6
suppress ASCII art;

diff -r 5cdcd51a4dad -r ff6caffcaed4 src/Pure/Isar/document_structure.scala
--- 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
         }