equal
deleted
inserted
replaced
33 (* XML resources *) |
33 (* XML resources *) |
34 |
34 |
35 val xml_file = XML.parse o File.read; |
35 val xml_file = XML.parse o File.read; |
36 |
36 |
37 fun xml_resource name = |
37 fun xml_resource name = |
38 let val script = "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name in |
38 let |
39 (case Isabelle_System.bash_output script of |
39 val res = |
40 (txt, 0) => XML.parse txt |
40 Isabelle_System.bash_process ("unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name); |
41 | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)) |
41 val rc = Process_Result.rc res; |
|
42 in |
|
43 res |> Process_Result.check |> Process_Result.out |> XML.parse |
|
44 handle ERROR _ => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc) |
42 end; |
45 end; |
43 |
46 |
44 |
47 |
45 (* actions *) |
48 (* actions *) |
46 |
49 |