src/Pure/Isar/isar.scala
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 29313 6852248da4b4
child 31797 203d5e61e3bc
permissions -rw-r--r--
use long names for old-style fold combinators;
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
29313
6852248da4b4 Isar.command: plain Position.id;
wenzelm
parents: 29192
diff changeset
     4
Isar document model.
28305
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
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29174
diff changeset
    10
class Isar(isabelle_system: IsabelleSystem, results: EventBus[IsabelleProcess.Result], args: String*)
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29174
diff changeset
    11
  extends IsabelleProcess(isabelle_system, results, args: _*)
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29174
diff changeset
    12
{
28305
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    13
  /* basic editor commands */
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    14
29313
6852248da4b4 Isar.command: plain Position.id;
wenzelm
parents: 29192
diff changeset
    15
  def create_command(id: String, text: String) =
6852248da4b4 Isar.command: plain Position.id;
wenzelm
parents: 29192
diff changeset
    16
    output_sync("Isar.command " + IsabelleSyntax.encode_string(id) + " " +
28305
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    17
      IsabelleSyntax.encode_string(text))
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    18
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    19
  def insert_command(prev: String, id: String) =
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    20
    output_sync("Isar.insert " + IsabelleSyntax.encode_string(prev) + " " +
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    21
      IsabelleSyntax.encode_string(id))
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    22
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    23
  def remove_command(id: String) =
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    24
    output_sync("Isar.remove " + IsabelleSyntax.encode_string(id))
5097b8c0f59f Isar toplevel editor model.
wenzelm
parents:
diff changeset
    25
}