equal
deleted
inserted
replaced
86 Pretty.str trace :: |
86 Pretty.str trace :: |
87 map (fn (name, status, context', stmt) => |
87 map (fn (name, status, context', stmt) => |
88 Pretty.big_list (name ^ " " ^ f status) |
88 Pretty.big_list (name ^ " " ^ f status) |
89 (Element.pretty_ctxt ctxt context' @ |
89 (Element.pretty_ctxt ctxt context' @ |
90 Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |> |
90 Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |> |
91 Pretty.writeln_chunks2 |
91 Pretty.chunks2 |> Pretty.writeln |
92 end; |
92 end; |
93 |
93 |
94 val _ = |
94 val _ = |
95 Outer_Syntax.command \<^command_keyword>\<open>spark_open_vcg\<close> |
95 Outer_Syntax.command \<^command_keyword>\<open>spark_open_vcg\<close> |
96 "open a new SPARK environment and load a SPARK-generated .vcg file" |
96 "open a new SPARK environment and load a SPARK-generated .vcg file" |