support for "use_theories";
authorwenzelm
Fri Mar 16 18:42:35 2018 +0100 (18 months ago)
changeset 67883171e7735ce25
parent 67882 7eb4c966e156
child 67884 43af581d7d8e
support for "use_theories";
src/Pure/PIDE/protocol.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Fri Mar 16 17:16:09 2018 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Mar 16 18:42:35 2018 +0100
     1.3 @@ -146,6 +146,11 @@
     1.4    {
     1.5      def total: Int = unprocessed + running + warned + failed + finished
     1.6      def ok: Boolean = failed == 0
     1.7 +
     1.8 +    def json: JSON.Object.T =
     1.9 +      JSON.Object("unprocessed" -> unprocessed, "running" -> running, "warned" -> warned,
    1.10 +        "failed" -> failed, "finished" -> finished, "consolidated" -> consolidated,
    1.11 +        "total" -> total, "ok" -> ok)
    1.12    }
    1.13  
    1.14    def node_status(
     2.1 --- a/src/Pure/Thy/thy_resources.scala	Fri Mar 16 17:16:09 2018 +0100
     2.2 +++ b/src/Pure/Thy/thy_resources.scala	Fri Mar 16 18:42:35 2018 +0100
     2.3 @@ -51,10 +51,11 @@
     2.4    }
     2.5  
     2.6    sealed case class Theories_Result(
     2.7 -    val requirements: List[Document.Node.Name],
     2.8 -    val version: Document.Version,
     2.9 -    val state: Document.State)
    2.10 +    val nodes: List[(Document.Node.Name, Protocol.Node_Status)],
    2.11 +    val state: Document.State,
    2.12 +    val version: Document.Version)
    2.13    {
    2.14 +    def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
    2.15    }
    2.16  
    2.17    class Session private[Thy_Resources](
    2.18 @@ -80,7 +81,10 @@
    2.19          val state = session.current_state()
    2.20          state.stable_tip_version match {
    2.21            case Some(version) if requirements.forall(state.node_consolidated(version, _)) =>
    2.22 -            try { result.fulfill(Theories_Result(requirements, version, state)) }
    2.23 +            def status(name: Document.Node.Name): Protocol.Node_Status =
    2.24 +              Protocol.node_status(state, version, name, version.nodes(name))
    2.25 +            val nodes = for (name <- requirements) yield (name -> status(name))
    2.26 +            try { result.fulfill(Theories_Result(nodes, state, version)) }
    2.27              catch { case _: IllegalStateException => }
    2.28            case _ =>
    2.29          }
     3.1 --- a/src/Pure/Tools/server.scala	Fri Mar 16 17:16:09 2018 +0100
     3.2 +++ b/src/Pure/Tools/server.scala	Fri Mar 16 18:42:35 2018 +0100
     3.3 @@ -91,6 +91,14 @@
     3.4                    val session = context.server.remove_session(id)
     3.5                    Server_Commands.Session_Stop.command(session)._1
     3.6                  })
     3.7 +          },
     3.8 +        "use_theories" ->
     3.9 +          { case (context, Server_Commands.Use_Theories(args)) =>
    3.10 +              context.make_task(task =>
    3.11 +                {
    3.12 +                  val session = context.server.the_session(args.session_id)
    3.13 +                  Server_Commands.Use_Theories.command(args, session, progress = task.progress)._1
    3.14 +                })
    3.15            })
    3.16  
    3.17      def unapply(name: String): Option[T] = table.get(name)
    3.18 @@ -465,14 +473,16 @@
    3.19    server =>
    3.20  
    3.21    private val _sessions = Synchronized(Map.empty[String, Thy_Resources.Session])
    3.22 +  def err_session(id: String): Nothing = error("No session " + Library.single_quote(id))
    3.23 +  def the_session(id: String): Thy_Resources.Session =
    3.24 +    _sessions.value.get(id) getOrElse err_session(id)
    3.25    def add_session(entry: (String, Thy_Resources.Session)) { _sessions.change(_ + entry) }
    3.26 -  def get_session(id: String): Option[Thy_Resources.Session] = { _sessions.value.get(id) }
    3.27    def remove_session(id: String): Thy_Resources.Session =
    3.28    {
    3.29      _sessions.change_result(sessions =>
    3.30        sessions.get(id) match {
    3.31          case Some(session) => (session, sessions - id)
    3.32 -        case None => error("No session " + Library.single_quote(id))
    3.33 +        case None => err_session(id)
    3.34        })
    3.35    }
    3.36  
     4.1 --- a/src/Pure/Tools/server_commands.scala	Fri Mar 16 17:16:09 2018 +0100
     4.2 +++ b/src/Pure/Tools/server_commands.scala	Fri Mar 16 18:42:35 2018 +0100
     4.3 @@ -10,6 +10,18 @@
     4.4  object Server_Commands
     4.5  {
     4.6    def default_preferences: String = Options.read_prefs()
     4.7 +  def default_qualifier: String = Sessions.DRAFT
     4.8 +
     4.9 +  def unapply_name_pos(json: JSON.T): Option[(String, Position.T)] =
    4.10 +    json match {
    4.11 +      case JSON.Value.String(name) => Some((name, Position.none))
    4.12 +      case JSON.Object(map) if map.keySet == Set("name", "pos") =>
    4.13 +      (map("name"), map("pos")) match {
    4.14 +        case (JSON.Value.String(name), Position.JSON(pos)) => Some((name, pos))
    4.15 +        case _ => None
    4.16 +      }
    4.17 +      case _ => None
    4.18 +    }
    4.19  
    4.20    object Session_Build
    4.21    {
    4.22 @@ -140,4 +152,39 @@
    4.23        else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json)
    4.24      }
    4.25    }
    4.26 +
    4.27 +  object Use_Theories
    4.28 +  {
    4.29 +    sealed case class Args(
    4.30 +      session_id: String,
    4.31 +      theories: List[(String, Position.T)],
    4.32 +      qualifier: String = default_qualifier,
    4.33 +      master_dir: String = "")
    4.34 +
    4.35 +    def unapply(json: JSON.T): Option[Args] =
    4.36 +      for {
    4.37 +        session_id <- JSON.string(json, "session_id")
    4.38 +        theories <- JSON.list(json, "theories", unapply_name_pos _)
    4.39 +        qualifier <- JSON.string_default(json, "qualifier", default_qualifier)
    4.40 +        master_dir <- JSON.string_default(json, "master_dir")
    4.41 +      }
    4.42 +      yield Args(session_id, theories, qualifier = qualifier, master_dir = master_dir)
    4.43 +
    4.44 +    def command(args: Args, session: Thy_Resources.Session, progress: Progress = No_Progress)
    4.45 +      : (JSON.Object.T, Thy_Resources.Theories_Result) =
    4.46 +    {
    4.47 +      val result =
    4.48 +        session.use_theories(args.theories, qualifier = args.qualifier,
    4.49 +          master_dir = args.master_dir, progress = progress)
    4.50 +
    4.51 +      val result_json =
    4.52 +        JSON.Object(
    4.53 +          "ok" -> result.ok,
    4.54 +          "nodes" ->
    4.55 +            (for ((name, st) <- result.nodes) yield
    4.56 +              JSON.Object("node_name" -> name.node, "theory" -> name.theory, "status" -> st.json)))
    4.57 +
    4.58 +      (result_json, result)
    4.59 +    }
    4.60 +  }
    4.61  }