more flexible session selection as in "isabelle jedit";
authorwenzelm
Thu Jul 26 15:19:56 2018 +0200 (12 months ago)
changeset 68690354c04092cd0
parent 68689 5b99b47b3b5f
child 68691 206966cbc2fc
more flexible session selection as in "isabelle jedit";
NEWS
src/Tools/VSCode/src/server.scala
     1.1 --- a/NEWS	Wed Jul 25 22:33:04 2018 +0200
     1.2 +++ b/NEWS	Thu Jul 26 15:19:56 2018 +0200
     1.3 @@ -148,6 +148,13 @@
     1.4  * HTML preview of theories and other file-formats similar to
     1.5  Isabelle/jEdit.
     1.6  
     1.7 +* Command-line tool "isabelle vscode_server" accepts the same options
     1.8 +-A, -R, -S, -i for session selection as "isabelle jedit". This is
     1.9 +relevant for isabelle.args configuration settings in VSCode. The former
    1.10 +option -A (explore all known session files) has been discontinued: it is
    1.11 +enabled by default, unless option -S is used to focus on a particular
    1.12 +spot in the session structure. INCOMPATIBILITY.
    1.13 +
    1.14  
    1.15  *** Document preparation ***
    1.16  
     2.1 --- a/src/Tools/VSCode/src/server.scala	Wed Jul 25 22:33:04 2018 +0200
     2.2 +++ b/src/Tools/VSCode/src/server.scala	Thu Jul 26 15:19:56 2018 +0200
     2.3 @@ -31,9 +31,12 @@
     2.4    val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args =>
     2.5    {
     2.6      try {
     2.7 -      var all_known = false
     2.8 +      var logic_ancestor: Option[String] = None
     2.9        var log_file: Option[Path] = None
    2.10 +      var logic_requirements = false
    2.11 +      var logic_focus = false
    2.12        var dirs: List[Path] = Nil
    2.13 +      var include_sessions: List[String] = Nil
    2.14        var logic = default_logic
    2.15        var modes: List[String] = Nil
    2.16        var options = Options.init()
    2.17 @@ -44,9 +47,12 @@
    2.18  Usage: isabelle vscode_server [OPTIONS]
    2.19  
    2.20    Options are:
    2.21 -    -A           explore theory name space of all known sessions (potentially slow)
    2.22 +    -A NAME      ancestor session for options -R and -S (default: parent)
    2.23      -L FILE      logging on FILE
    2.24 +    -R NAME      build image with requirements from other sessions
    2.25 +    -S NAME      like option -R, with focus on selected session
    2.26      -d DIR       include session directory
    2.27 +    -i NAME      include session in name-space of theories
    2.28      -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
    2.29      -m MODE      add print mode for output
    2.30      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    2.31 @@ -55,9 +61,12 @@
    2.32  
    2.33    Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
    2.34  """,
    2.35 -        "A" -> (_ => all_known = true),
    2.36 +        "A:" -> (arg => logic_ancestor = Some(arg)),
    2.37          "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
    2.38 +        "R:" -> (arg => { logic = arg; logic_requirements = true }),
    2.39 +        "S:" -> (arg => { logic = arg; logic_requirements = true; logic_focus = true }),
    2.40          "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
    2.41 +        "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
    2.42          "l:" -> (arg => logic = arg),
    2.43          "m:" -> (arg => modes = arg :: modes),
    2.44          "o:" -> (arg => options = options + arg),
    2.45 @@ -71,7 +80,9 @@
    2.46        val channel = new Channel(System.in, System.out, log, verbose)
    2.47        val server =
    2.48          new Server(channel, options, session_name = logic, session_dirs = dirs,
    2.49 -          all_known = all_known, modes = modes, system_mode = system_mode, log = log)
    2.50 +          include_sessions = include_sessions, session_ancestor = logic_ancestor,
    2.51 +          session_requirements = logic_requirements, session_focus = logic_focus,
    2.52 +          all_known = !logic_focus, modes = modes, system_mode = system_mode, log = log)
    2.53  
    2.54        // prevent spurious garbage on the main protocol channel
    2.55        val orig_out = System.out
    2.56 @@ -95,6 +106,10 @@
    2.57    options: Options,
    2.58    session_name: String = Server.default_logic,
    2.59    session_dirs: List[Path] = Nil,
    2.60 +  include_sessions: List[String] = Nil,
    2.61 +  session_ancestor: Option[String] = None,
    2.62 +  session_requirements: Boolean = false,
    2.63 +  session_focus: Boolean = false,
    2.64    all_known: Boolean = false,
    2.65    modes: List[String] = Nil,
    2.66    system_mode: Boolean = false,
    2.67 @@ -242,35 +257,41 @@
    2.68  
    2.69    def init(id: Protocol.Id)
    2.70    {
    2.71 -    def reply(err: String)
    2.72 +    def reply_ok(msg: String)
    2.73      {
    2.74 -      channel.write(Protocol.Initialize.reply(id, err))
    2.75 -      if (err == "")
    2.76 -        channel.writeln("Welcome to Isabelle/" + session_name + " (" + Distribution.version + ")")
    2.77 -      else channel.error_message(err)
    2.78 +      channel.write(Protocol.Initialize.reply(id, ""))
    2.79 +      channel.writeln(msg)
    2.80 +    }
    2.81 +
    2.82 +    def reply_error(msg: String)
    2.83 +    {
    2.84 +      channel.write(Protocol.Initialize.reply(id, msg))
    2.85 +      channel.error_message(msg)
    2.86      }
    2.87  
    2.88      val try_session =
    2.89        try {
    2.90 -        if (!Build.build(options, build_heap = true, no_build = true,
    2.91 -            system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
    2.92 -        {
    2.93 -          val start_msg = "Build started for Isabelle/" + session_name + " ..."
    2.94 +        val base_info =
    2.95 +          Sessions.base_info(
    2.96 +            options, session_name, dirs = session_dirs, include_sessions = include_sessions,
    2.97 +            session_ancestor = session_ancestor, session_requirements = session_requirements,
    2.98 +            session_focus = session_focus, all_known = all_known)
    2.99 +        val session_base = base_info.check_base
   2.100 +
   2.101 +        def build(no_build: Boolean = false): Build.Results =
   2.102 +          Build.build(options, build_heap = true, no_build = no_build, system_mode = system_mode,
   2.103 +            dirs = session_dirs, infos = base_info.infos, sessions = List(base_info.session))
   2.104 +
   2.105 +        if (!build(no_build = true).ok) {
   2.106 +          val start_msg = "Build started for Isabelle/" + base_info.session + " ..."
   2.107            val fail_msg = "Session build failed -- prover process remains inactive!"
   2.108  
   2.109            val progress = channel.progress(verbose = true)
   2.110            progress.echo(start_msg); channel.writeln(start_msg)
   2.111  
   2.112 -          if (!Build.build(options, progress = progress, build_heap = true,
   2.113 -              system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
   2.114 -          {
   2.115 -            progress.echo(fail_msg); error(fail_msg)
   2.116 -          }
   2.117 +          if (!build().ok) { progress.echo(fail_msg); error(fail_msg) }
   2.118          }
   2.119  
   2.120 -        val session_base =
   2.121 -          Sessions.base_info(
   2.122 -            options, session_name, dirs = session_dirs, all_known = all_known).check_base
   2.123          val resources = new VSCode_Resources(options, session_base, log)
   2.124            {
   2.125              override def commit(change: Session.Change): Unit =
   2.126 @@ -279,11 +300,13 @@
   2.127            }
   2.128  
   2.129          val session_options = options.bool("editor_output_state") = true
   2.130 -        Some(new Session(session_options, resources))
   2.131 +        val session = new Session(session_options, resources)
   2.132 +
   2.133 +        Some((base_info, session))
   2.134        }
   2.135 -      catch { case ERROR(msg) => reply(msg); None }
   2.136 +      catch { case ERROR(msg) => reply_error(msg); None }
   2.137  
   2.138 -    for (session <- try_session) {
   2.139 +    for ((base_info, session) <- try_session) {
   2.140        session_.change(_ => Some(session))
   2.141  
   2.142        session.commands_changed += prover_output
   2.143 @@ -296,16 +319,16 @@
   2.144          Session.Consumer(getClass.getName) {
   2.145            case Session.Ready =>
   2.146              session.phase_changed -= session_phase
   2.147 -            reply("")
   2.148 +            reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")")
   2.149            case Session.Terminated(result) if !result.ok =>
   2.150              session.phase_changed -= session_phase
   2.151 -            reply("Prover startup failed: return code " + result.rc)
   2.152 +            reply_error("Prover startup failed: return code " + result.rc)
   2.153            case _ =>
   2.154          }
   2.155        session.phase_changed += session_phase
   2.156  
   2.157 -      Isabelle_Process.start(session, options,
   2.158 -        logic = session_name, dirs = session_dirs, modes = modes)
   2.159 +      Isabelle_Process.start(session, options, modes = modes,
   2.160 +        sessions_structure = Some(base_info.sessions_structure), logic = base_info.session)
   2.161      }
   2.162    }
   2.163