tuned signature;
authorwenzelm
Wed Jul 10 22:04:57 2013 +0200 (2013-07-10 ago)
changeset 5258231467a4b1466
parent 52581 99835e3abca4
child 52583 0a7240d88e09
tuned signature;
src/Pure/PIDE/protocol.scala
src/Pure/System/invoke_scala.scala
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Jul 10 21:54:43 2013 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Jul 10 22:04:57 2013 +0200
     1.3 @@ -308,15 +308,15 @@
     1.4    /* commands */
     1.5  
     1.6    def define_command(command: Command): Unit =
     1.7 -    input("Document.define_command",
     1.8 +    protocol_command("Document.define_command",
     1.9        Document_ID(command.id), encode(command.name), encode(command.source))
    1.10  
    1.11  
    1.12    /* document versions */
    1.13  
    1.14 -  def discontinue_execution() { input("Document.discontinue_execution") }
    1.15 +  def discontinue_execution() { protocol_command("Document.discontinue_execution") }
    1.16  
    1.17 -  def cancel_execution() { input("Document.cancel_execution") }
    1.18 +  def cancel_execution() { protocol_command("Document.cancel_execution") }
    1.19  
    1.20    def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
    1.21      edits: List[Document.Edit_Command])
    1.22 @@ -346,7 +346,7 @@
    1.23          pair(string, encode_edit(name))(name.node, edit)
    1.24        })
    1.25        YXML.string_of_body(encode_edits(edits)) }
    1.26 -    input("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
    1.27 +    protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
    1.28    }
    1.29  
    1.30    def remove_versions(versions: List[Document.Version])
    1.31 @@ -354,7 +354,7 @@
    1.32      val versions_yxml =
    1.33        { import XML.Encode._
    1.34          YXML.string_of_body(list(long)(versions.map(_.id))) }
    1.35 -    input("Document.remove_versions", versions_yxml)
    1.36 +    protocol_command("Document.remove_versions", versions_yxml)
    1.37    }
    1.38  
    1.39  
    1.40 @@ -362,6 +362,6 @@
    1.41  
    1.42    def dialog_result(serial: Long, result: String)
    1.43    {
    1.44 -    input("Document.dialog_result", Properties.Value.Long(serial), result)
    1.45 +    protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
    1.46    }
    1.47  }
     2.1 --- a/src/Pure/System/invoke_scala.scala	Wed Jul 10 21:54:43 2013 +0200
     2.2 +++ b/src/Pure/System/invoke_scala.scala	Wed Jul 10 22:04:57 2013 +0200
     2.3 @@ -76,7 +76,7 @@
     2.4      id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit = synchronized
     2.5    {
     2.6      if (futures.isDefinedAt(id)) {
     2.7 -      prover.input("Invoke_Scala.fulfill", id, tag.toString, res)
     2.8 +      prover.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
     2.9        futures -= id
    2.10      }
    2.11    }
     3.1 --- a/src/Pure/System/isabelle_process.ML	Wed Jul 10 21:54:43 2013 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Jul 10 22:04:57 2013 +0200
     3.3 @@ -48,15 +48,15 @@
     3.4  fun protocol_command name cmd =
     3.5    Synchronized.change commands (fn cmds =>
     3.6     (if not (Symtab.defined cmds name) then ()
     3.7 -    else warning ("Redefining Isabelle process command " ^ quote name);
     3.8 +    else warning ("Redefining Isabelle protocol command " ^ quote name);
     3.9      Symtab.update (name, cmd) cmds));
    3.10  
    3.11  fun run_command name args =
    3.12    (case Symtab.lookup (Synchronized.value commands) name of
    3.13 -    NONE => error ("Undefined Isabelle process command " ^ quote name)
    3.14 +    NONE => error ("Undefined Isabelle protocol command " ^ quote name)
    3.15    | SOME cmd =>
    3.16        (Runtime.debugging cmd args handle exn =>
    3.17 -        error ("Isabelle process protocol failure: " ^ quote name ^ "\n" ^
    3.18 +        error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
    3.19            ML_Compiler.exn_message exn)));
    3.20  
    3.21  end;
     4.1 --- a/src/Pure/System/isabelle_process.scala	Wed Jul 10 21:54:43 2013 +0200
     4.2 +++ b/src/Pure/System/isabelle_process.scala	Wed Jul 10 22:04:57 2013 +0200
     4.3 @@ -354,15 +354,15 @@
     4.4  
     4.5    /** main methods **/
     4.6  
     4.7 -  def input_bytes(name: String, args: Array[Byte]*): Unit =
     4.8 +  def protocol_command_raw(name: String, args: Array[Byte]*): Unit =
     4.9      command_input._2 ! Input_Chunks(UTF8.string_bytes(name) :: args.toList)
    4.10  
    4.11 -  def input(name: String, args: String*)
    4.12 +  def protocol_command(name: String, args: String*)
    4.13    {
    4.14      receiver(new Input(name, args.toList))
    4.15 -    input_bytes(name, args.map(UTF8.string_bytes): _*)
    4.16 +    protocol_command_raw(name, args.map(UTF8.string_bytes): _*)
    4.17    }
    4.18  
    4.19    def options(opts: Options): Unit =
    4.20 -    input("Isabelle_Process.options", YXML.string_of_body(opts.encode))
    4.21 +    protocol_command("Isabelle_Process.options", YXML.string_of_body(opts.encode))
    4.22  }