more explicit build_session args;
authorwenzelm
Sat Mar 18 16:15:37 2017 +0100 (2017-03-18)
changeset 65307c1ba192b4f96
parent 65306 eab556c6037d
child 65308 8f58102afa22
more explicit build_session args;
support both command-line and PIDE version;
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.ML	Sat Mar 18 14:30:03 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Sat Mar 18 16:15:37 2017 +0100
     1.3 @@ -99,7 +99,7 @@
     1.4    | [] => raise Output.Protocol_Message props);
     1.5  
     1.6  
     1.7 -(* build *)
     1.8 +(* build theories *)
     1.9  
    1.10  fun build_theories symbols last_timing master_dir (options, thys) =
    1.11    let
    1.12 @@ -129,23 +129,44 @@
    1.13          " (undefined " ^ commas conds ^ ")\n")
    1.14    end;
    1.15  
    1.16 -fun build args_file =
    1.17 +
    1.18 +(* build session *)
    1.19 +
    1.20 +datatype args = Args of
    1.21 + {symbol_codes: (string * int) list,
    1.22 +  command_timings: Properties.T list,
    1.23 +  do_output: bool,
    1.24 +  verbose: bool,
    1.25 +  browser_info: Path.T,
    1.26 +  document_files: (Path.T * Path.T) list,
    1.27 +  graph_file: Path.T,
    1.28 +  parent_name: string,
    1.29 +  chapter: string,
    1.30 +  name: string,
    1.31 +  master_dir: Path.T,
    1.32 +  theories: (Options.T * (string * Position.T) list) list};
    1.33 +
    1.34 +fun decode_args yxml =
    1.35    let
    1.36 -    val _ = SHA1.test_samples ();
    1.37 -
    1.38 +    open XML.Decode;
    1.39      val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
    1.40 -          (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =
    1.41 -      File.read (Path.explode args_file) |> YXML.parse_body |>
    1.42 -        let open XML.Decode in
    1.43 -          pair (list (pair string int)) (pair (list properties) (pair bool
    1.44 -            (pair bool (pair string (pair (list (pair string string)) (pair string
    1.45 -              (pair string (pair string (pair string
    1.46 -              ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))
    1.47 -        end;
    1.48 +      (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, theories))))))))))) =
    1.49 +      pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
    1.50 +        (pair (list (pair string string)) (pair string (pair string (pair string (pair string
    1.51 +          (pair string (((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))))
    1.52 +      (YXML.parse_body yxml);
    1.53 +  in
    1.54 +    Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
    1.55 +      verbose = verbose, browser_info = Path.explode browser_info,
    1.56 +      document_files = map (apply2 Path.explode) document_files,
    1.57 +      graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
    1.58 +      name = name, master_dir = Path.explode master_dir, theories = theories}
    1.59 +  end;
    1.60  
    1.61 +fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
    1.62 +    document_files, graph_file, parent_name, chapter, name, master_dir, theories}) =
    1.63 +  let
    1.64      val symbols = HTML.make_symbols symbol_codes;
    1.65 -    val _ = Options.load_default ();
    1.66 -    val _ = Isabelle_Process.init_options ();
    1.67  
    1.68      val _ = writeln ("\fSession.name = " ^ name);
    1.69      val _ =
    1.70 @@ -153,31 +174,50 @@
    1.71          symbols
    1.72          do_output
    1.73          (Options.default_bool "browser_info")
    1.74 -        (Path.explode browser_info)
    1.75 +        browser_info
    1.76          (Options.default_string "document")
    1.77          (Options.default_string "document_output")
    1.78          (Present.document_variants (Options.default_string "document_variants"))
    1.79 -        (map (apply2 Path.explode) document_files)
    1.80 -        (Path.explode graph_file)
    1.81 -        parent_name (chapter, name)
    1.82 +        document_files
    1.83 +        graph_file
    1.84 +        parent_name
    1.85 +        (chapter, name)
    1.86          verbose;
    1.87  
    1.88      val last_timing = get_timings (fold update_timings command_timings empty_timings);
    1.89  
    1.90      val res1 =
    1.91        theories |>
    1.92 -        (List.app (build_theories symbols last_timing Path.current)
    1.93 +        (List.app (build_theories symbols last_timing master_dir)
    1.94            |> session_timing name verbose
    1.95 -          |> Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
    1.96            |> Exn.capture);
    1.97      val res2 = Exn.capture Session.finish ();
    1.98      val _ = Par_Exn.release_all [res1, res2];
    1.99 +  in () end;
   1.100  
   1.101 +(*command-line tool*)
   1.102 +fun build args_file =
   1.103 +  let
   1.104 +    val _ = SHA1.test_samples ();
   1.105 +    val _ = Options.load_default ();
   1.106 +    val _ = Isabelle_Process.init_options ();
   1.107 +    val args = decode_args (File.read (Path.explode args_file));
   1.108 +    val _ =
   1.109 +      Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
   1.110 +        build_session args;
   1.111      val _ = Options.reset_default ();
   1.112    in () end;
   1.113  
   1.114 -
   1.115 -(* PIDE protocol *)
   1.116 +(*PIDE version*)
   1.117 +val _ =
   1.118 +  Isabelle_Process.protocol_command "build_session"
   1.119 +    (fn [id, yxml] =>
   1.120 +      let
   1.121 +        val args = decode_args yxml;
   1.122 +        val result = (build_session args; "") handle exn =>
   1.123 +          (Runtime.exn_message exn handle _ (*sic!*) =>
   1.124 +            "Exception raised, but failed to print details!");
   1.125 +    in Output.protocol_message (Markup.build_theories_result id) [result] end | _ => raise Match);
   1.126  
   1.127  val _ =
   1.128    Isabelle_Process.protocol_command "build_theories"
     2.1 --- a/src/Pure/Tools/build.scala	Sat Mar 18 14:30:03 2017 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Sat Mar 18 16:15:37 2017 +0100
     2.3 @@ -162,12 +162,12 @@
     2.4                import XML.Encode._
     2.5                pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
     2.6                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
     2.7 -                pair(string, pair(string, pair(string,
     2.8 -                list(pair(Options.encode, list(Path.encode)))))))))))))(
     2.9 +                pair(string, pair(string, pair(string, pair(Path.encode,
    2.10 +                list(pair(Options.encode, list(Path.encode))))))))))))))(
    2.11                (Symbol.codes, (command_timings, (do_output, (verbose,
    2.12                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    2.13 -                (parent, (info.chapter, (name,
    2.14 -                theories)))))))))))
    2.15 +                (parent, (info.chapter, (name, (Path.current,
    2.16 +                theories))))))))))))
    2.17              }))
    2.18  
    2.19          val eval =