equal
deleted
inserted
replaced
80 val settings_dir = Path.explode("$JEDIT_SETTINGS") |
80 val settings_dir = Path.explode("$JEDIT_SETTINGS") |
81 Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager")) |
81 Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager")) |
82 |
82 |
83 if (!(settings_dir + Path.explode("perspective.xml")).is_file) { |
83 if (!(settings_dir + Path.explode("perspective.xml")).is_file) { |
84 File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"), |
84 File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"), |
85 """<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""") |
85 """<DOCKING LEFT="" TOP="" RIGHT="isabelle-documentation" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""") |
86 File.write(settings_dir + Path.explode("perspective.xml"), |
86 File.write(settings_dir + Path.explode("perspective.xml"), |
87 """<?xml version="1.0" encoding="UTF-8" ?> |
87 """<?xml version="1.0" encoding="UTF-8" ?> |
88 <!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd"> |
88 <!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd"> |
89 <PERSPECTIVE> |
89 <PERSPECTIVE> |
90 <VIEW PLAIN="FALSE"> |
90 <VIEW PLAIN="FALSE"> |