# HG changeset patch
# User wenzelm
# Date 1419863939 -3600
# Node ID 73a6403637b343d79d842b233ad9131210580994
# Parent  f8588372d70e4cdcadf7280cef3160dd8a5e7000
more toplevel pretty printing;

diff -r f8588372d70e -r 73a6403637b3 src/Pure/General/scan.ML
--- 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
diff -r f8588372d70e -r 73a6403637b3 src/Pure/ROOT.ML
--- 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";
diff -r f8588372d70e -r 73a6403637b3 src/Pure/Syntax/lexicon.ML
--- 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;