equal
deleted
inserted
replaced
33 } |
33 } |
34 |
34 |
35 |
35 |
36 /* list systems */ |
36 /* list systems */ |
37 |
37 |
38 def proper_lines(content: HTTP.Content): List[String] = |
|
39 Library.trim_split_lines(content.text).filterNot(_.startsWith("%")) |
|
40 |
|
41 def list_systems(url: URL): List[String] = |
38 def list_systems(url: URL): List[String] = |
42 proper_lines(post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY"))) |
39 post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY")).text_lines |
43 |
40 |
44 object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true) |
41 object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true) |
45 { |
42 { |
46 val here = Scala_Project.here |
43 val here = Scala_Project.here |
47 def apply(url: String): String = cat_lines(list_systems(Url(url))) |
44 def apply(url: String): String = cat_lines(list_systems(Url(url))) |