src/Pure/Isar/isar.scala
author wenzelm
Thu, 01 Jan 2009 10:42:48 +0100
changeset 29283 f4743512b12d
parent 29192 082ee2a01a6d
child 29313 6852248da4b4
permissions -rw-r--r--
updated sessions;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28305
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Isar/isar.scala
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
     3
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
     4
Isar toplevel editor model.
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
     5
*/
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
     6
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
     7
package isabelle
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
     8
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
     9
import java.util.Properties
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    10
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    11
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29174
diff changeset
    12
class Isar(isabelle_system: IsabelleSystem, results: EventBus[IsabelleProcess.Result], args: String*)
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29174
diff changeset
    13
  extends IsabelleProcess(isabelle_system, results, args: _*)
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29174
diff changeset
    14
{
28305
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    15
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    16
  /* basic editor commands */
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    17
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    18
  def create_command(props: Properties, text: String) =
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    19
    output_sync("Isar.command " + IsabelleSyntax.encode_properties(props) + " " +
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    20
      IsabelleSyntax.encode_string(text))
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    21
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    22
  def insert_command(prev: String, id: String) =
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    23
    output_sync("Isar.insert " + IsabelleSyntax.encode_string(prev) + " " +
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    24
      IsabelleSyntax.encode_string(id))
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    25
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    26
  def remove_command(id: String) =
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    27
    output_sync("Isar.remove " + IsabelleSyntax.encode_string(id))
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    28
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    29
}