diff --git a/src/Pure/General/untyped.scala b/src/Pure/General/untyped.scala
--- a/src/Pure/General/untyped.scala
+++ b/src/Pure/General/untyped.scala
@@ -1,53 +1,60 @@
 /*  Title:      Pure/General/untyped.scala
     Author:     Makarius
 
 Untyped, unscoped, unchecked access to JVM objects.
 */
 
 package isabelle
 
 
-import java.lang.reflect.{Method, Field}
+import java.lang.reflect.{Constructor, Method, Field}
 
 
 object Untyped
 {
+  def constructor[C](c: Class[C], arg_types: Class[_]*): Constructor[C] =
+  {
+    val con = c.getDeclaredConstructor(arg_types: _*)
+    con.setAccessible(true)
+    con
+  }
+
   def method(c: Class[_], name: String, arg_types: Class[_]*): Method =
   {
     val m = c.getDeclaredMethod(name, arg_types: _*)
     m.setAccessible(true)
     m
   }
 
   def classes(obj: AnyRef): Iterator[Class[_ <: AnyRef]] = new Iterator[Class[_ <: AnyRef]] {
     private var next_elem: Class[_ <: AnyRef] = obj.getClass
     def hasNext(): Boolean = next_elem != null
     def next(): Class[_ <: AnyRef] = {
       val c = next_elem
       next_elem = c.getSuperclass.asInstanceOf[Class[_ <: AnyRef]]
       c
     }
   }
 
   def field(obj: AnyRef, x: String): Field =
   {
     val iterator =
       for {
         c <- classes(obj)
         field <- c.getDeclaredFields.iterator
         if field.getName == x
       } yield {
         field.setAccessible(true)
         field
       }
     if (iterator.hasNext) iterator.next
     else error("No field " + quote(x) + " for " + obj)
   }
 
   def get[A](obj: AnyRef, x: String): A =
     if (obj == null) null.asInstanceOf[A]
     else field(obj, x).get(obj).asInstanceOf[A]
 
   def set[A](obj: AnyRef, x: String, y: A): Unit =
     field(obj, x).set(obj, y)
 }
diff --git a/src/Pure/Tools/spell_checker.scala b/src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala
+++ b/src/Pure/Tools/spell_checker.scala
@@ -1,291 +1,289 @@
 /*  Title:      Pure/Tools/spell_checker.scala
     Author:     Makarius
 
 Spell checker with completion, based on JOrtho (see
 https://sourceforge.net/projects/jortho).
 */
 
 package isabelle
 
 
 import java.lang.Class
 
 import scala.collection.mutable
 import scala.annotation.tailrec
 import scala.collection.immutable.SortedMap
 
 
 object Spell_Checker
 {
   /* words within text */
 
   def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean)
     : List[Text.Info[String]] =
   {
     val result = new mutable.ListBuffer[Text.Info[String]]
     var offset = 0
 
     def apostrophe(c: Int): Boolean =
       c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'')
 
     @tailrec def scan(pred: Int => Boolean)
     {
       if (offset < text.length) {
         val c = text.codePointAt(offset)
         if (pred(c)) {
           offset += Character.charCount(c)
           scan(pred)
         }
       }
     }
 
     while (offset < text.length) {
       scan(c => !Character.isLetter(c))
       val start = offset
       scan(c => Character.isLetterOrDigit(c) || apostrophe(c))
       val stop = offset
       if (stop - start >= 2) {
         val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop))
         if (mark(info)) result += info
       }
     }
     result.toList
   }
 
   def current_word(rendering: Rendering, range: Text.Range): Option[Text.Info[String]] =
   {
     for {
       spell_range <- rendering.spell_checker_point(range)
       text <- rendering.get_text(spell_range)
       info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
     } yield info
   }
 
 
   /* dictionaries */
 
   class Dictionary private[Spell_Checker](val path: Path)
   {
     val lang: String = path.drop_ext.file_name
     val user_path: Path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
     override def toString: String = lang
   }
 
   private object Decl
   {
     def apply(name: String, include: Boolean): String =
       if (include) name else "-" + name
 
     def unapply(decl: String): Option[(String, Boolean)] =
     {
       val decl1 = decl.trim
       if (decl1 == "" || decl1.startsWith("#")) None
       else
         Library.try_unprefix("-", decl1.trim) match {
           case None => Some((decl1, true))
           case Some(decl2) => Some((decl2, false))
         }
     }
   }
 
   def dictionaries(): List[Dictionary] =
     for {
       path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
       if path.is_file
     } yield new Dictionary(path)
 
 
   /* create spell checker */
 
   def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary)
 
   private sealed case class Update(include: Boolean, permanent: Boolean)
 }
 
 
 class Spell_Checker private(dictionary: Spell_Checker.Dictionary)
 {
   override def toString: String = dictionary.toString
 
 
   /* main dictionary content */
 
   private var dict = new Object
   private var updates = SortedMap.empty[String, Spell_Checker.Update]
 
   private def included_iterator(): Iterator[String] =
     for {
       (word, upd) <- updates.iterator
       if upd.include
     } yield word
 
   private def excluded(word: String): Boolean =
     updates.get(word) match {
       case Some(upd) => !upd.include
       case None => false
     }
 
   private def load()
   {
     val main_dictionary = split_lines(File.read_gzip(dictionary.path))
 
     val permanent_updates =
       if (dictionary.user_path.is_file)
         for {
           Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
         } yield (word, Spell_Checker.Update(include, true))
       else Nil
 
     updates =
       updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++
         permanent_updates
 
     val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
-    val factory_constructor = factory_class.getConstructor()
-    factory_constructor.setAccessible(true)
-    val factory = factory_constructor.newInstance()
+    val factory = Untyped.constructor(factory_class).newInstance()
 
     val add = Untyped.method(factory_class, "add", classOf[String])
 
     for {
       word <- main_dictionary.iterator ++ included_iterator()
       if !excluded(word)
     } add.invoke(factory, word)
 
     dict = Untyped.method(factory_class, "create").invoke(factory)
   }
   load()
 
   private def save()
   {
     val permanent_decls =
       (for {
         (word, upd) <- updates.iterator
         if upd.permanent
       } yield Spell_Checker.Decl(word, upd.include)).toList
 
     if (permanent_decls.nonEmpty || dictionary.user_path.is_file) {
       val header = """# User updates for spell-checker dictionary
 #
 #   * each line contains at most one word
 #   * extra blanks are ignored
 #   * lines starting with "#" are stripped
 #   * lines starting with "-" indicate excluded words
 #
 #:mode=text:encoding=UTF-8:
 
 """
       Isabelle_System.make_directory(dictionary.user_path.expand.dir)
       File.write(dictionary.user_path, header + cat_lines(permanent_decls))
     }
   }
 
   def update(word: String, include: Boolean, permanent: Boolean)
   {
     updates += (word -> Spell_Checker.Update(include, permanent))
 
     if (include) {
       if (permanent) save()
       Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word)
     }
     else { save(); load() }
   }
 
   def reset()
   {
     updates = SortedMap.empty
     load()
   }
 
   def reset_enabled(): Int =
     updates.valuesIterator.count(upd => !upd.permanent)
 
 
   /* check known words */
 
   def contains(word: String): Boolean =
     Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]).
       invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
 
   def check(word: String): Boolean =
     word match {
       case Word.Case(c) if c != Word.Lowercase =>
         contains(word) || contains(Word.lowercase(word))
       case _ =>
         contains(word)
     }
 
   def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] =
     Spell_Checker.marked_words(base, text, info => !check(info.info))
 
 
   /* completion: suggestions for unknown words */
 
   private def suggestions(word: String): Option[List[String]] =
   {
     val res =
       Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
         invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
     if (res.isEmpty) None else Some(res)
   }
 
   def complete(word: String): List[String] =
     if (check(word)) Nil
     else {
       val word_case = Word.Case.unapply(word)
       def recover_case(s: String) =
         word_case match {
           case Some(c) => Word.Case(c, s)
           case None => s
         }
       val result =
         word_case match {
           case Some(c) if c != Word.Lowercase =>
             suggestions(word) orElse suggestions(Word.lowercase(word))
           case _ =>
             suggestions(word)
         }
       result.getOrElse(Nil).map(recover_case)
     }
 
   def completion(rendering: Rendering, caret: Text.Offset): Option[Completion.Result] =
   {
     val caret_range = rendering.before_caret_range(caret)
     for {
       word <- Spell_Checker.current_word(rendering, caret_range)
       words = complete(word.info)
       if words.nonEmpty
       descr = "(from dictionary " + quote(dictionary.toString) + ")"
       items =
         words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
     } yield Completion.Result(word.range, word.info, false, items)
   }
 }
 
 class Spell_Checker_Variable
 {
   private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None)
   private var current_spell_checker = no_spell_checker
 
   def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 }
 
   def update(options: Options): Unit = synchronized {
     if (options.bool("spell_checker")) {
       val lang = options.string("spell_checker_dictionary")
       if (current_spell_checker._1 != lang) {
         Spell_Checker.dictionaries.find(_.lang == lang) match {
           case Some(dictionary) =>
             val spell_checker =
               Exn.capture { Spell_Checker(dictionary) } match {
                 case Exn.Res(spell_checker) => Some(spell_checker)
                 case Exn.Exn(_) => None
               }
             current_spell_checker = (lang, spell_checker)
           case None =>
             current_spell_checker = no_spell_checker
         }
       }
     }
     else current_spell_checker = no_spell_checker
   }
 }