equal
deleted
inserted
replaced
64 val isabelle_process_options = Isabelle_System.tmp_file("options") |
64 val isabelle_process_options = Isabelle_System.tmp_file("options") |
65 File.write(isabelle_process_options, YXML.string_of_body(options.encode)) |
65 File.write(isabelle_process_options, YXML.string_of_body(options.encode)) |
66 val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) |
66 val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) |
67 val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") |
67 val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") |
68 |
68 |
|
69 val print_depth = ML_Syntax.print_int(options.int("ML_print_depth")) |
69 val eval_process = |
70 val eval_process = |
70 if (heaps.isEmpty) |
71 if (heaps.isEmpty) |
71 List("PolyML.print_depth 20") |
72 List("PolyML.print_depth " + print_depth) |
72 else |
73 else |
73 channel match { |
74 channel match { |
74 case None => |
75 case None => |
75 List("(ML_Pretty.print_depth 20; Isabelle_Process.init_options ())") |
76 List("(ML_Pretty.print_depth " + print_depth + "; Isabelle_Process.init_options ())") |
76 case Some(ch) => |
77 case Some(ch) => |
77 List("(ML_Pretty.print_depth 20; Isabelle_Process.init_protocol " + |
78 List("(ML_Pretty.print_depth " + print_depth + "; Isabelle_Process.init_protocol " + |
78 ML_Syntax.print_string0(ch.server_name) + ")") |
79 ML_Syntax.print_string0(ch.server_name) + ")") |
79 } |
80 } |
80 |
81 |
81 // ISABELLE_TMP |
82 // ISABELLE_TMP |
82 val isabelle_tmp = Isabelle_System.tmp_dir("process") |
83 val isabelle_tmp = Isabelle_System.tmp_dir("process") |