package PIDE_examples


import isabelle._

import scala.actors.Actor._


object Ex
{
  object Theory_Session
  {
    def apply(
      logic: String = "",
      imports: List[String] = List("Main"),
      verbose: Boolean = false): Theory_Session =
    {
      Isabelle_System.init()

      val logic1 =
        if (logic != null && logic != "") logic
        else Isabelle_System.getenv_strict("ISABELLE_LOGIC")

      new Theory_Session(logic1, imports, verbose)
    }
  }

  class Theory_Session private(logic: String, imports: List[String], verbose: Boolean)
    extends Session()
  {
    override val output_delay = Time.seconds(0.01)
    override val prune_size = 1  // number of old document versions to retain


    /* theory node */

    private val theory_name = "Theory"

    private val node_name =
    {
      val id = Document.new_id().toString
      val path = Thy_Header.thy_path(Path.root + Path.basic("dummy" + id) + Path.basic(theory_name))
      Document.Node.Name(path)
    }
    private val header_text: String =
      "theory " + quote(theory_name) + " imports " + imports.map(quote).mkString(" ") + " begin\n"
    private val header: Document.Node_Header = Exn.Res(Thy_Header.read(header_text))
    private val perspective = Text.Perspective(List(Text.Range(0, Integer.MAX_VALUE)))


    /* main actor */

    private case object Get_Startup
    private case object Get_Theory

    private val main_actor = actor {
      var startup_result: Option[Exn.Result[Unit]] = None
      var theory_result: Option[Exn.Result[Unit]] = None

      loop {
        react {
          case message: Isabelle_Process.Message =>
            System.err.println(message.toString)

          case phase: Session.Phase =>
            phase match {
              case Session.Failed =>
                startup_result =
                  Some(Exn.Exn(ERROR("Failed to start Isabelle process:\n" + syslog)))

              case Session.Ready =>
                startup_result = Some(Exn.Res(()))

              case Session.Shutdown =>  // FIXME

              case _ =>
            }

          case _: Session.Commands_Changed =>
            if (!theory_result.isDefined) {
              val snapshot = this.snapshot(node_name, Nil)
              if (!snapshot.is_outdated) {
                snapshot.node.commands.find(_.name == "theory").map(snapshot.command_state) match {
                  case None =>
                  case Some(state) =>
                    val err =
                      (for ((_, t) <- state.results.iterator; if Isar_Document.is_error(t))
                        yield Pretty.string_of(List(t))).mkString("\n")

                    Isar_Document.command_status(state.status) match {
                      case Isar_Document.Finished =>
                        theory_result = Some(if (err == "") Exn.Res(()) else Exn.Exn(ERROR(err)))

                      case Isar_Document.Failed =>
                        theory_result = Some(Exn.Exn(ERROR(err)))

                      case _ =>
                    }
                }
              }
            }

          case Get_Startup if startup_result.isDefined => reply(startup_result.get)

          case Get_Theory if theory_result.isDefined => reply(theory_result.get)

          case bad if startup_result.isDefined && theory_result.isDefined =>
            System.err.println("main_actor: ignoring bad message " + bad)
        }
      }
    }


    /* init */

    if (verbose) raw_messages += main_actor
    phase_changed += main_actor
    commands_changed += main_actor

    start(List(logic))
    Exn.release((main_actor !? Get_Startup).asInstanceOf[Exn.Result[Unit]])

    init_node(node_name, header, perspective, header_text)
    Exn.release((main_actor !? Get_Theory).asInstanceOf[Exn.Result[Unit]])
  }
}