src/Tools/jEdit/lib/Tools/jedit
changeset 69756 1907222d974e
parent 69637 f3b564a13236
child 69762 58fb0d779583
equal deleted inserted replaced
69755:2fc85ce1f557 69756:1907222d974e
    34   "src/graphview_dockable.scala"
    34   "src/graphview_dockable.scala"
    35   "src/info_dockable.scala"
    35   "src/info_dockable.scala"
    36   "src/isabelle.scala"
    36   "src/isabelle.scala"
    37   "src/isabelle_encoding.scala"
    37   "src/isabelle_encoding.scala"
    38   "src/isabelle_export.scala"
    38   "src/isabelle_export.scala"
       
    39   "src/isabelle_vfs.scala"
    39   "src/isabelle_options.scala"
    40   "src/isabelle_options.scala"
    40   "src/isabelle_sidekick.scala"
    41   "src/isabelle_sidekick.scala"
    41   "src/jedit_bibtex.scala"
    42   "src/jedit_bibtex.scala"
    42   "src/jedit_editor.scala"
    43   "src/jedit_editor.scala"
    43   "src/jedit_lib.scala"
    44   "src/jedit_lib.scala"