equal
deleted
inserted
replaced
73 if (heaps.isEmpty) |
73 if (heaps.isEmpty) |
74 List("PolyML.print_depth 10") |
74 List("PolyML.print_depth 10") |
75 else |
75 else |
76 channel match { |
76 channel match { |
77 case None => |
77 case None => |
78 List("(default_print_depth 10; Isabelle_Process.init_options ())") |
78 List("(ML_Pretty.print_depth 10; Isabelle_Process.init_options ())") |
79 case Some(ch) => |
79 case Some(ch) => |
80 List("(default_print_depth 10; Isabelle_Process.init_protocol " + |
80 List("(ML_Pretty.print_depth 10; Isabelle_Process.init_protocol " + |
81 ML_Syntax.print_string0(ch.server_name) + ")") |
81 ML_Syntax.print_string0(ch.server_name) + ")") |
82 } |
82 } |
83 |
83 |
84 // ISABELLE_TMP |
84 // ISABELLE_TMP |
85 val isabelle_tmp = Isabelle_System.tmp_dir("process") |
85 val isabelle_tmp = Isabelle_System.tmp_dir("process") |