src/Pure/PIDE/session.scala
changeset 56864 0446c7ac2e32
parent 56799 00b13fb87b3a
child 57651 10df45dd14da
equal deleted inserted replaced
56863:5fdb61a9a010 56864:0446c7ac2e32
    96 
    96 
    97   /* protocol handlers */
    97   /* protocol handlers */
    98 
    98 
    99   abstract class Protocol_Handler
    99   abstract class Protocol_Handler
   100   {
   100   {
       
   101     def start(prover: Prover): Unit = {}
   101     def stop(prover: Prover): Unit = {}
   102     def stop(prover: Prover): Unit = {}
   102     val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
   103     val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
   103   }
   104   }
   104 
   105 
   105   class Protocol_Handlers(
   106   class Protocol_Handlers(
   120         }
   121         }
   121 
   122 
   122       val (handlers2, functions2) =
   123       val (handlers2, functions2) =
   123         try {
   124         try {
   124           val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
   125           val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
       
   126           new_handler.start(prover)
       
   127 
   125           val new_functions =
   128           val new_functions =
   126             for ((a, f) <- new_handler.functions.toList) yield
   129             for ((a, f) <- new_handler.functions.toList) yield
   127               (a, (msg: Prover.Protocol_Output) => f(prover, msg))
   130               (a, (msg: Prover.Protocol_Output) => f(prover, msg))
   128 
   131 
   129           val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
   132           val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a