src/Tools/jEdit/src/prover/Prover.scala
author immler@in.tum.de
Mon, 12 Jan 2009 20:49:37 +0100
changeset 34475 f963335dbc6b
parent 34471 1dac47492863
child 34477 e561d0915f28
permissions -rw-r--r--
implemented IsabelleSideKickParser.complete removed Plugin.prover (to avoid NoSuchElementException)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34404
diff changeset
     1
/*
aad6834ba380 added some headers and comments;
wenzelm
parents: 34404
diff changeset
     2
 * Higher-level prover communication
aad6834ba380 added some headers and comments;
wenzelm
parents: 34404
diff changeset
     3
 *
aad6834ba380 added some headers and comments;
wenzelm
parents: 34404
diff changeset
     4
 * @author Johannes Hölzl, TU Munich
aad6834ba380 added some headers and comments;
wenzelm
parents: 34404
diff changeset
     5
 * @author Fabian Immler, TU Munich
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
     6
 * @author Makarius
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34404
diff changeset
     7
 */
aad6834ba380 added some headers and comments;
wenzelm
parents: 34404
diff changeset
     8
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     9
package isabelle.prover
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    10
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    11
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    12
import java.util.Properties
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    13
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    14
import scala.collection.mutable.{HashMap, HashSet}
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34471
diff changeset
    15
import scala.collection.immutable.{TreeSet}
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    16
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
    17
import org.gjt.sp.util.Log
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
    18
34443
f2e13329cc49 dynamic instances Isabelle.system, Isabelle.symbols;
wenzelm
parents: 34410
diff changeset
    19
import isabelle.proofdocument.{ProofDocument, Text, Token}
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    20
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    21
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    22
class Prover(isabelle_system: IsabelleSystem, isabelle_symbols: Symbol.Interpretation)
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    23
{
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    24
  private var _logic = isabelle_system.getenv_strict("ISABELLE_LOGIC")
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    25
  private var process: Isar = null
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    26
  private var commands = new HashMap[String, Command]
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    27
34465
ccadbf63e320 added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents: 34462
diff changeset
    28
  val decl_info = new EventBus[(String, String)]
34471
1dac47492863 decl_info: cover both commands and keywords, with kind;
wenzelm
parents: 34466
diff changeset
    29
  val command_decls = new HashMap[String, String] {
1dac47492863 decl_info: cover both commands and keywords, with kind;
wenzelm
parents: 34466
diff changeset
    30
    override def +=(entry: (String, String)) = {
1dac47492863 decl_info: cover both commands and keywords, with kind;
wenzelm
parents: 34466
diff changeset
    31
      decl_info.event(entry)
1dac47492863 decl_info: cover both commands and keywords, with kind;
wenzelm
parents: 34466
diff changeset
    32
      super.+=(entry)
34465
ccadbf63e320 added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents: 34462
diff changeset
    33
    }
ccadbf63e320 added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents: 34462
diff changeset
    34
  }
34471
1dac47492863 decl_info: cover both commands and keywords, with kind;
wenzelm
parents: 34466
diff changeset
    35
  val keyword_decls = new HashSet[String] {
1dac47492863 decl_info: cover both commands and keywords, with kind;
wenzelm
parents: 34466
diff changeset
    36
    override def +=(name: String) = {
1dac47492863 decl_info: cover both commands and keywords, with kind;
wenzelm
parents: 34466
diff changeset
    37
      decl_info.event(name, OuterKeyword.MINOR)
1dac47492863 decl_info: cover both commands and keywords, with kind;
wenzelm
parents: 34466
diff changeset
    38
      super.+=(name)
34465
ccadbf63e320 added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents: 34462
diff changeset
    39
    }
ccadbf63e320 added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents: 34462
diff changeset
    40
  }
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34471
diff changeset
    41
  var _completions = new TreeSet[String]
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34471
diff changeset
    42
  def completions = _completions
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34471
diff changeset
    43
  /* // TODO: ask Makarius to make Interpretation.symbols public (here: read-only as 'symbol_map')
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34471
diff changeset
    44
  val map = isabelle.jedit.Isabelle.symbols.symbol_map
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34471
diff changeset
    45
  for(xsymb <- map.keys) {
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34471
diff changeset
    46
    _completions += xsymb
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34471
diff changeset
    47
    if(map(xsymb).get("abbrev").isDefined) _completions += map(xsymb)("abbrev")
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34471
diff changeset
    48
  }
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34471
diff changeset
    49
  */
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34471
diff changeset
    50
  decl_info += (k_v => _completions += k_v._1)
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34471
diff changeset
    51
  
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    52
  private var initialized = false
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    53
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
    54
  val activated = new EventBus[Unit]
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
    55
  val command_info = new EventBus[Command]
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
    56
  val output_info = new EventBus[String]
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    57
  var document: Document = null
34399
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34397
diff changeset
    58
34444
a245f6cc3105 replaced inUIThread by scala-style swing/swing_async combinators;
wenzelm
parents: 34443
diff changeset
    59
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
    60
  def command_change(c: Command) = Swing.now { command_info.event(c) }
34399
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34397
diff changeset
    61
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    62
  private def handle_result(r: IsabelleProcess.Result) = {
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    63
    val id = if (r.props != null) r.props.getProperty(Markup.ID) else null
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    64
    val st = if (id != null) commands.getOrElse(id, null) else null
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    65
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    66
    if (r.kind == IsabelleProcess.Kind.STDOUT || r.kind == IsabelleProcess.Kind.STDIN)
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
    67
      Swing.now { output_info.event(r.result) }
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    68
    else if (r.kind == IsabelleProcess.Kind.WRITELN && !initialized) {
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    69
      initialized = true
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
    70
      Swing.now {
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    71
        if (document != null) {
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    72
          document.activate()
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
    73
          activated.event(())
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    74
        }
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    75
      }
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    76
    }
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    77
    else {
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    78
      val tree = YXML.parse_failsafe(isabelle_symbols.decode(r.result))
34458
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34456
diff changeset
    79
      if (st == null || (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)) {
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    80
        r.kind match {
34404
98155c35d252 delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents: 34401
diff changeset
    81
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    82
          case IsabelleProcess.Kind.STATUS =>
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    83
            //{{{ handle all kinds of status messages here
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    84
            tree match {
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    85
              case XML.Elem(Markup.MESSAGE, _, elems) =>
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    86
                for (elem <- elems) {
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    87
                  elem match {
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    88
                    //{{{
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    89
                    // command status
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    90
                    case XML.Elem(Markup.FINISHED, _, _) =>
34458
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34456
diff changeset
    91
                      st.status = Command.Status.FINISHED
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
    92
                      command_change(st)
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    93
                    case XML.Elem(Markup.UNPROCESSED, _, _) =>
34458
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34456
diff changeset
    94
                      st.status = Command.Status.UNPROCESSED
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
    95
                      command_change(st)
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    96
                    case XML.Elem(Markup.FAILED, _, _) =>
34458
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34456
diff changeset
    97
                      st.status = Command.Status.FAILED
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
    98
                      command_change(st)
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
    99
                    case XML.Elem(Markup.DISPOSED, _, _) =>
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   100
                      document.prover.commands.removeKey(st.id)
34458
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34456
diff changeset
   101
                      st.status = Command.Status.REMOVED
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   102
                      command_change(st)
34399
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34397
diff changeset
   103
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   104
                    // command and keyword declarations
34471
1dac47492863 decl_info: cover both commands and keywords, with kind;
wenzelm
parents: 34466
diff changeset
   105
                    case XML.Elem(Markup.COMMAND_DECL,
1dac47492863 decl_info: cover both commands and keywords, with kind;
wenzelm
parents: 34466
diff changeset
   106
                        (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
1dac47492863 decl_info: cover both commands and keywords, with kind;
wenzelm
parents: 34466
diff changeset
   107
                      command_decls += (name -> kind)
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   108
                    case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   109
                      keyword_decls += name
34404
98155c35d252 delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents: 34401
diff changeset
   110
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   111
                    // other markup
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   112
                    case XML.Elem(kind,
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   113
                        (Markup.OFFSET, offset) :: (Markup.END_OFFSET, end_offset) ::
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   114
                             (Markup.ID, markup_id) :: _, _) =>
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   115
                      val begin = Int.unbox(java.lang.Integer.valueOf(offset)) - 1
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   116
                      val end = Int.unbox(java.lang.Integer.valueOf(end_offset)) - 1
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   117
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   118
                      val command =
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   119
                        // outer syntax: no id in props
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   120
                        if (st == null) commands.getOrElse(markup_id, null)
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   121
                        // inner syntax: id from props
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   122
                        else st
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   123
                      command.root_node.insert(command.node_from(kind, begin, end))
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   124
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   125
                    case _ =>
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   126
                    //}}}
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   127
                  }
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   128
                }
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   129
              case _ =>
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   130
            }
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   131
            //}}}
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   132
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   133
          case IsabelleProcess.Kind.ERROR if st != null =>
34458
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34456
diff changeset
   134
            if (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34456
diff changeset
   135
              st.status = Command.Status.FAILED
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   136
            st.add_result(tree)
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   137
            command_change(st)
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   138
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   139
          case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   140
            | IsabelleProcess.Kind.WARNING if st != null =>
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   141
            st.add_result(tree)
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   142
            command_change(st)
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   143
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   144
          case _ =>
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   145
        }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   146
      }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   147
    }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   148
  }
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   149
34370
e0679b361a0e register to buffer all messages
immler@in.tum.de
parents: 34359
diff changeset
   150
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   151
  def start(logic: String) {
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   152
    if (logic != null) _logic = logic
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   153
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   154
    val results = new EventBus[IsabelleProcess.Result]
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   155
    results += handle_result
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   156
    results.logger = Log.log(Log.ERROR, null, _)
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   157
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   158
    process = new Isar(isabelle_system, results, "-m", "xsymbols", _logic)
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   159
  }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   160
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   161
  def stop() {
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   162
    process.kill
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   163
  }
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   164
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   165
  def set_document(text: Text, path: String) {
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   166
    this.document = new Document(text, this)
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   167
    process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   168
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   169
    document.structural_changes += (changes => {
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   170
      for (cmd <- changes.removedCommands) remove(cmd)
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   171
      for (cmd <- changes.addedCommands) send(cmd)
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   172
    })
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   173
    if (initialized) {
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   174
      document.activate()
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34454
diff changeset
   175
      activated.event(())
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   176
    }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   177
  }
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   178
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   179
  private def send(cmd: Command) {
34458
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34456
diff changeset
   180
    cmd.status = Command.Status.UNPROCESSED
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34444
diff changeset
   181
    commands.put(cmd.id, cmd)
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   182
34443
f2e13329cc49 dynamic instances Isabelle.system, Isabelle.symbols;
wenzelm
parents: 34410
diff changeset
   183
    val content = isabelle_symbols.encode(document.getContent(cmd))
34459
b08299e7bbe6 adapted Isar.command;
wenzelm
parents: 34458
diff changeset
   184
    process.create_command(cmd.id, content)
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   185
    process.insert_command(if (cmd.previous == null) "" else cmd.previous.id, cmd.id)
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   186
  }
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   187
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   188
  def remove(cmd: Command) {
34458
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34456
diff changeset
   189
    cmd.status = Command.Status.REMOVE
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   190
    process.remove_command(cmd.id)
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   191
  }
34453
dfa99a91951b eliminated hardwired string constants;
wenzelm
parents: 34452
diff changeset
   192
}