src/Tools/VSCode/src/server.scala
changeset 64733 20174e871623
parent 64727 13e37567a0d6
child 64737 9fc965612459
     1.1 --- a/src/Tools/VSCode/src/server.scala	Sun Jan 01 12:20:51 2017 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Sun Jan 01 13:15:50 2017 +0100
     1.3 @@ -32,6 +32,7 @@
     1.4        var logic = default_logic
     1.5        var modes: List[String] = Nil
     1.6        var options = Options.init()
     1.7 +      var system_mode = false
     1.8  
     1.9        def text_length_choice: String =
    1.10          commas(Text.Length.encodings.map(
    1.11 @@ -47,6 +48,7 @@
    1.12      -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
    1.13      -m MODE      add print mode for output
    1.14      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    1.15 +    -s           system build mode for session image
    1.16  
    1.17    Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
    1.18  """,
    1.19 @@ -55,18 +57,15 @@
    1.20          "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    1.21          "l:" -> (arg => logic = arg),
    1.22          "m:" -> (arg => modes = arg :: modes),
    1.23 -        "o:" -> (arg => options = options + arg))
    1.24 +        "o:" -> (arg => options = options + arg),
    1.25 +        "s" -> (_ => system_mode = true))
    1.26  
    1.27        val more_args = getopts(args)
    1.28        if (more_args.nonEmpty) getopts.usage()
    1.29  
    1.30 -      if (!Build.build(options = options, build_heap = true, no_build = true,
    1.31 -            dirs = dirs, sessions = List(logic)).ok)
    1.32 -        error("Missing logic image " + quote(logic))
    1.33 -
    1.34        val log = Logger.make(log_file)
    1.35        val channel = new Channel(System.in, System.out, log)
    1.36 -      val server = new Server(channel, options, text_length, logic, dirs, modes, log)
    1.37 +      val server = new Server(channel, options, text_length, logic, dirs, modes, system_mode, log)
    1.38  
    1.39        // prevent spurious garbage on the main protocol channel
    1.40        val orig_out = System.out
    1.41 @@ -92,6 +91,7 @@
    1.42    session_name: String = Server.default_logic,
    1.43    session_dirs: List[Path] = Nil,
    1.44    modes: List[String] = Nil,
    1.45 +  system_mode: Boolean = false,
    1.46    log: Logger = No_Logger)
    1.47  {
    1.48    /* prover session */
    1.49 @@ -180,6 +180,22 @@
    1.50  
    1.51      val try_session =
    1.52        try {
    1.53 +        if (!Build.build(options = options, build_heap = true, no_build = true,
    1.54 +              system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
    1.55 +        {
    1.56 +          val start_msg = "Build started for Isabelle/" + session_name + " ..."
    1.57 +          val fail_msg = "Session build failed -- prover process remains inactive!"
    1.58 +
    1.59 +          val progress = channel.make_progress(verbose = true)
    1.60 +          progress.echo(start_msg); channel.writeln(start_msg)
    1.61 +
    1.62 +          if (!Build.build(options = options, progress = progress, build_heap = true,
    1.63 +              system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
    1.64 +          {
    1.65 +            progress.echo(fail_msg); error(fail_msg)
    1.66 +          }
    1.67 +        }
    1.68 +
    1.69          val content = Build.session_content(options, false, session_dirs, session_name)
    1.70          val resources =
    1.71            new VSCode_Resources(options, text_length, content.loaded_theories,