51 recodes it temporarily as UTF-16. This works for well-formed Unicode |
51 recodes it temporarily as UTF-16. This works for well-formed Unicode |
52 text, but not for arbitrary byte strings. In such cases, the bash |
52 text, but not for arbitrary byte strings. In such cases, the bash |
53 script should write tempory files, managed by Isabelle/ML operations |
53 script should write tempory files, managed by Isabelle/ML operations |
54 like Isabelle_System.with_tmp_file to create a file name and |
54 like Isabelle_System.with_tmp_file to create a file name and |
55 File.read to retrieve its content. |
55 File.read to retrieve its content. |
|
56 |
|
57 - Just like any other Scala function invoked from ML, |
|
58 Isabelle_System.bash_process requires a proper PIDE session context. |
|
59 This could be a regular batch session (e.g. "isabelle build"), a |
|
60 PIDE editor session (e.g. "isabelle jedit"), or headless PIDE (e.g. |
|
61 "isabelle dump" or "isabelle server"). Note that old "isabelle |
|
62 console" or raw "isabelle process" don't have that. |
56 |
63 |
57 New Process_Result.timing works as in Isabelle/Scala, based on direct |
64 New Process_Result.timing works as in Isabelle/Scala, based on direct |
58 measurements of the bash_process wrapper in C: elapsed time is always |
65 measurements of the bash_process wrapper in C: elapsed time is always |
59 available, CPU time is only available on Linux and macOS, GC time is |
66 available, CPU time is only available on Linux and macOS, GC time is |
60 unavailable. |
67 unavailable. |