equal
deleted
inserted
replaced
12 extends Isabelle_Process(isabelle_system, results, args: _*) |
12 extends Isabelle_Process(isabelle_system, results, args: _*) |
13 { |
13 { |
14 /* basic editor commands */ |
14 /* basic editor commands */ |
15 |
15 |
16 def create_command(id: String, text: String) = |
16 def create_command(id: String, text: String) = |
17 output_sync("Isar.command " + IsabelleSyntax.encode_string(id) + " " + |
17 output_sync("Isar.command " + Isabelle_Syntax.encode_string(id) + " " + |
18 IsabelleSyntax.encode_string(text)) |
18 Isabelle_Syntax.encode_string(text)) |
19 |
19 |
20 def insert_command(prev: String, id: String) = |
20 def insert_command(prev: String, id: String) = |
21 output_sync("Isar.insert " + IsabelleSyntax.encode_string(prev) + " " + |
21 output_sync("Isar.insert " + Isabelle_Syntax.encode_string(prev) + " " + |
22 IsabelleSyntax.encode_string(id)) |
22 Isabelle_Syntax.encode_string(id)) |
23 |
23 |
24 def remove_command(id: String) = |
24 def remove_command(id: String) = |
25 output_sync("Isar.remove " + IsabelleSyntax.encode_string(id)) |
25 output_sync("Isar.remove " + Isabelle_Syntax.encode_string(id)) |
26 } |
26 } |