src/Tools/jEdit/lib/Tools/jedit
changeset 49570 2265456f6131
parent 49566 66cbf8bb4693
child 49600 2b114b9d9d34
equal deleted inserted replaced
49569:7b6aaf446496 49570:2265456f6131
     9 
     9 
    10 declare -a SOURCES=(
    10 declare -a SOURCES=(
    11   "src/dockable.scala"
    11   "src/dockable.scala"
    12   "src/document_model.scala"
    12   "src/document_model.scala"
    13   "src/document_view.scala"
    13   "src/document_view.scala"
       
    14   "src/graphview_dockable.scala"
    14   "src/html_panel.scala"
    15   "src/html_panel.scala"
    15   "src/graph_dockable.scala"
       
    16   "src/hyperlink.scala"
    16   "src/hyperlink.scala"
    17   "src/isabelle_encoding.scala"
    17   "src/isabelle_encoding.scala"
    18   "src/isabelle_logic.scala"
    18   "src/isabelle_logic.scala"
    19   "src/isabelle_options.scala"
    19   "src/isabelle_options.scala"
    20   "src/isabelle_rendering.scala"
    20   "src/isabelle_rendering.scala"