src/Pure/Isar/isar.scala
author wenzelm
Fri, 19 Dec 2008 20:37:29 +0100
changeset 29140 e7ac5bb20aed
parent 28305 5097b8c0f59f
child 29174 d4058295affb
permissions -rw-r--r--
removed Ids;
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
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    12
class Isar(args: String*) extends IsabelleProcess(args: _*) {
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    13
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    14
  /* basic editor commands */
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    15
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    16
  def create_command(props: Properties, text: String) =
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    17
    output_sync("Isar.command " + IsabelleSyntax.encode_properties(props) + " " +
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    18
      IsabelleSyntax.encode_string(text))
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    19
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    20
  def insert_command(prev: String, id: String) =
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    21
    output_sync("Isar.insert " + IsabelleSyntax.encode_string(prev) + " " +
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    22
      IsabelleSyntax.encode_string(id))
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    23
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    24
  def remove_command(id: String) =
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    25
    output_sync("Isar.remove " + IsabelleSyntax.encode_string(id))
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    26
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    27
}