Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
compactified output
authorhaftmann
Fri, 04 Aug 2017 08:12:37 +0200
changeset 66332 489667636064
parent 66331 f773691617c0
child 66333 30c1639a343a
compactified output
src/Pure/Isar/code.ML file | annotate | diff | comparison | revisions
src/Tools/Code/code_preproc.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/code.ML	Thu Aug 03 12:50:03 2017 +0200
+++ b/src/Pure/Isar/code.ML	Fri Aug 04 08:12:37 2017 +0200
@@ -1072,7 +1072,7 @@
       end;
 
 fun pretty_cert _ (Nothing _) =
-      [Pretty.str "(unimplemented)"]
+      []
   | pretty_cert thy (cert as Equations _) =
       (map_filter
         (Option.map (Thm.pretty_thm_global thy o
--- a/src/Tools/Code/code_preproc.ML	Thu Aug 03 12:50:03 2017 +0200
+++ b/src/Tools/Code/code_preproc.ML	Fri Aug 04 08:12:37 2017 +0200
@@ -306,7 +306,9 @@
     AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
     |> (map o apfst) (Code.string_of_const thy)
     |> sort (string_ord o apply2 fst)
-    |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
+    |> (map o apsnd) (Code.pretty_cert thy)
+    |> filter_out (null o snd)
+    |> map (fn (s, ps) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: ps))
     |> Pretty.chunks
   end;
isabelle