equal
deleted
inserted
replaced
98 (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]" |
98 (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]" |
99 } |
99 } |
100 def is_raw = Kind.is_raw(kind) |
100 def is_raw = Kind.is_raw(kind) |
101 def is_control = Kind.is_control(kind) |
101 def is_control = Kind.is_control(kind) |
102 def is_system = Kind.is_system(kind) |
102 def is_system = Kind.is_system(kind) |
|
103 |
|
104 def cache(table: XML.Cache): Result = |
|
105 new Result(kind, table.cache_props(props), table(body)) |
103 } |
106 } |
104 } |
107 } |
105 |
108 |
106 |
109 |
107 class Isabelle_Process(system: Isabelle_System, receiver: Actor, args: String*) |
110 class Isabelle_Process(system: Isabelle_System, receiver: Actor, args: String*) |