--- a/src/Pure/General/scan.ML Sun Dec 28 22:10:09 2014 +0100
+++ b/src/Pure/General/scan.ML Mon Dec 29 15:38:59 2014 +0100
@@ -328,7 +328,7 @@
val content = dest path' lex;
in append (if tip then rev path' :: content else content) end) tab [];
-val dest_lexicon = map implode o dest [];
+val dest_lexicon = sort_strings o map implode o dest [];
fun merge_lexicons (lex1, lex2) =
if pointer_eq (lex1, lex2) then lex1
--- a/src/Pure/ROOT.ML Sun Dec 28 22:10:09 2014 +0100
+++ b/src/Pure/ROOT.ML Mon Dec 29 15:38:59 2014 +0100
@@ -346,6 +346,7 @@
(* ML toplevel pretty printing *)
toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
+toplevel_pp ["Scan", "lexicon"] "Lexicon.pp_lexicon";
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
toplevel_pp ["Position", "T"] "Pretty.position";
--- a/src/Pure/Syntax/lexicon.ML Sun Dec 28 22:10:09 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML Mon Dec 29 15:38:59 2014 +0100
@@ -66,6 +66,7 @@
val is_marked: string -> bool
val dummy_type: term
val fun_type: term
+ val pp_lexicon: Scan.lexicon -> Pretty.T
end;
structure Lexicon: LEXICON =
@@ -451,4 +452,10 @@
val dummy_type = Syntax.const (mark_type "dummy");
val fun_type = Syntax.const (mark_type "fun");
+
+(* toplevel pretty printing *)
+
+val pp_lexicon =
+ Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon;
+
end;