src/Pure/System/session.scala
changeset 43748 c70bd78ec83c
parent 43746 a41f618c641d
child 44156 6aa25b80e1a5
     1.1 --- a/src/Pure/System/session.scala	Mon Jul 11 15:56:30 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Mon Jul 11 16:48:02 2011 +0200
     1.3 @@ -255,12 +255,20 @@
     1.4        }
     1.5  
     1.6        result.properties match {
     1.7 -        case Position.Id(state_id) =>
     1.8 +        case Position.Id(state_id) if !result.is_raw =>
     1.9            try {
    1.10              val st = global_state.change_yield(_.accumulate(state_id, result.message))
    1.11              command_change_buffer ! st.command
    1.12            }
    1.13 -          catch { case _: Document.State.Fail => bad_result(result) }
    1.14 +          catch {
    1.15 +            case _: Document.State.Fail => bad_result(result)
    1.16 +          }
    1.17 +        case Markup.Invoke_Scala(name, id) if result.is_raw =>
    1.18 +          Future.fork {
    1.19 +            val arg = XML.content(result.body).mkString
    1.20 +            val (tag, res) = Invoke_Scala.method(name, arg)
    1.21 +            prover.get.invoke_scala(id, tag, res)
    1.22 +          }
    1.23          case _ =>
    1.24            if (result.is_syslog) {
    1.25              reverse_syslog ::= result.message
    1.26 @@ -289,9 +297,8 @@
    1.27                case _ => bad_result(result)
    1.28              }
    1.29            }
    1.30 -          else if (result.is_raw) { } // FIXME
    1.31            else bad_result(result)
    1.32 -        }
    1.33 +      }
    1.34      }
    1.35      //}}}
    1.36