src/Pure/Tools/spell_checker.scala
changeset 72611 e48d93811ed7
parent 71951 9644811b5b0a
child 73093 3a27e6f83ce1
equal deleted inserted replaced
72606:4c8295f2f849 72611:e48d93811ed7
   173 #   * lines starting with "-" indicate excluded words
   173 #   * lines starting with "-" indicate excluded words
   174 #
   174 #
   175 #:mode=text:encoding=UTF-8:
   175 #:mode=text:encoding=UTF-8:
   176 
   176 
   177 """
   177 """
   178       Isabelle_System.mkdirs(dictionary.user_path.expand.dir)
   178       Isabelle_System.make_directory(dictionary.user_path.expand.dir)
   179       File.write(dictionary.user_path, header + cat_lines(permanent_decls))
   179       File.write(dictionary.user_path, header + cat_lines(permanent_decls))
   180     }
   180     }
   181   }
   181   }
   182 
   182 
   183   def update(word: String, include: Boolean, permanent: Boolean)
   183   def update(word: String, include: Boolean, permanent: Boolean)