equal
deleted
inserted
replaced
16 fun get_url () = Options.default_string \<^system_option>\<open>SystemOnTPTP\<close> |
16 fun get_url () = Options.default_string \<^system_option>\<open>SystemOnTPTP\<close> |
17 |
17 |
18 fun list_systems () = |
18 fun list_systems () = |
19 let |
19 let |
20 val url = get_url () |
20 val url = get_url () |
21 val systems = split_lines (\<^scala>\<open>SystemOnTPTP.list_systems\<close> url) |
21 val systems = trim_split_lines (\<^scala>\<open>SystemOnTPTP.list_systems\<close> url) |
22 in {url = url, systems = systems} end |
22 in {url = url, systems = systems} end |
23 |
23 |
24 end |
24 end |