automatically build session image;
authorwenzelm
Sun Jan 01 13:15:50 2017 +0100 (2017-01-01)
changeset 6473320174e871623
parent 64732 00f3c4bef2e0
child 64734 12558536d977
automatically build session image;
src/Tools/VSCode/README.md
src/Tools/VSCode/src/channel.scala
src/Tools/VSCode/src/server.scala
     1.1 --- a/src/Tools/VSCode/README.md	Sun Jan 01 12:20:51 2017 +0100
     1.2 +++ b/src/Tools/VSCode/README.md	Sun Jan 01 13:15:50 2017 +0100
     1.3 @@ -6,8 +6,6 @@
     1.4  
     1.5  ## Run ##
     1.6  
     1.7 -* shell> `isabelle build -b HOL`
     1.8 -
     1.9  * Extensions: search "Isabelle 0.1.0", click "Install"
    1.10  
    1.11  * Preferences / User settings / edit settings.json: e.g.
     2.1 --- a/src/Tools/VSCode/src/channel.scala	Sun Jan 01 12:20:51 2017 +0100
     2.2 +++ b/src/Tools/VSCode/src/channel.scala	Sun Jan 01 13:15:50 2017 +0100
     2.3 @@ -99,6 +99,16 @@
     2.4    def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) }
     2.5  
     2.6  
     2.7 +  /* progress */
     2.8 +
     2.9 +  def make_progress(verbose: Boolean = false): Progress =
    2.10 +    new Progress {
    2.11 +      override def echo(msg: String): Unit = log_writeln(msg)
    2.12 +      override def theory(session: String, theory: String): Unit =
    2.13 +        if (verbose) echo(session + ": theory " + theory)
    2.14 +    }
    2.15 +
    2.16 +
    2.17    /* diagnostics */
    2.18  
    2.19    def diagnostics(uri: String, diagnostics: List[Protocol.Diagnostic]): Unit =
     3.1 --- a/src/Tools/VSCode/src/server.scala	Sun Jan 01 12:20:51 2017 +0100
     3.2 +++ b/src/Tools/VSCode/src/server.scala	Sun Jan 01 13:15:50 2017 +0100
     3.3 @@ -32,6 +32,7 @@
     3.4        var logic = default_logic
     3.5        var modes: List[String] = Nil
     3.6        var options = Options.init()
     3.7 +      var system_mode = false
     3.8  
     3.9        def text_length_choice: String =
    3.10          commas(Text.Length.encodings.map(
    3.11 @@ -47,6 +48,7 @@
    3.12      -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
    3.13      -m MODE      add print mode for output
    3.14      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    3.15 +    -s           system build mode for session image
    3.16  
    3.17    Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
    3.18  """,
    3.19 @@ -55,18 +57,15 @@
    3.20          "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    3.21          "l:" -> (arg => logic = arg),
    3.22          "m:" -> (arg => modes = arg :: modes),
    3.23 -        "o:" -> (arg => options = options + arg))
    3.24 +        "o:" -> (arg => options = options + arg),
    3.25 +        "s" -> (_ => system_mode = true))
    3.26  
    3.27        val more_args = getopts(args)
    3.28        if (more_args.nonEmpty) getopts.usage()
    3.29  
    3.30 -      if (!Build.build(options = options, build_heap = true, no_build = true,
    3.31 -            dirs = dirs, sessions = List(logic)).ok)
    3.32 -        error("Missing logic image " + quote(logic))
    3.33 -
    3.34        val log = Logger.make(log_file)
    3.35        val channel = new Channel(System.in, System.out, log)
    3.36 -      val server = new Server(channel, options, text_length, logic, dirs, modes, log)
    3.37 +      val server = new Server(channel, options, text_length, logic, dirs, modes, system_mode, log)
    3.38  
    3.39        // prevent spurious garbage on the main protocol channel
    3.40        val orig_out = System.out
    3.41 @@ -92,6 +91,7 @@
    3.42    session_name: String = Server.default_logic,
    3.43    session_dirs: List[Path] = Nil,
    3.44    modes: List[String] = Nil,
    3.45 +  system_mode: Boolean = false,
    3.46    log: Logger = No_Logger)
    3.47  {
    3.48    /* prover session */
    3.49 @@ -180,6 +180,22 @@
    3.50  
    3.51      val try_session =
    3.52        try {
    3.53 +        if (!Build.build(options = options, build_heap = true, no_build = true,
    3.54 +              system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
    3.55 +        {
    3.56 +          val start_msg = "Build started for Isabelle/" + session_name + " ..."
    3.57 +          val fail_msg = "Session build failed -- prover process remains inactive!"
    3.58 +
    3.59 +          val progress = channel.make_progress(verbose = true)
    3.60 +          progress.echo(start_msg); channel.writeln(start_msg)
    3.61 +
    3.62 +          if (!Build.build(options = options, progress = progress, build_heap = true,
    3.63 +              system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
    3.64 +          {
    3.65 +            progress.echo(fail_msg); error(fail_msg)
    3.66 +          }
    3.67 +        }
    3.68 +
    3.69          val content = Build.session_content(options, false, session_dirs, session_name)
    3.70          val resources =
    3.71            new VSCode_Resources(options, text_length, content.loaded_theories,