From 413a5e0b1fde6296a09a6651cef7948bc408c6e4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 3 Nov 2000 12:19:43 +0000 Subject: [PATCH] The interface sorts the entryes in the trees --- helm/interface/Makefile | 7 +++++++ helm/interface/mmlinterface.ml | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/helm/interface/Makefile b/helm/interface/Makefile index 2b892e2d9..981454830 100644 --- a/helm/interface/Makefile +++ b/helm/interface/Makefile @@ -169,6 +169,13 @@ start-xaland: examples/style/annotatedpres.xsl examples/style/theory_content.xsl \ examples/style/theory_pres.xsl +start-xaland-old: + java xaland 12345 12346 \ + examples/style/style_prima_del_linguaggio_naturale/rootcontent.xsl \ + examples/style/style_prima_del_linguaggio_naturale/annotatedpres.xsl \ + examples/style/style_prima_del_linguaggio_naturale/theory_content.xsl \ + examples/style/style_prima_del_linguaggio_naturale/theory_pres.xsl + start-xaland3: java xaland 12347 12348 examples/style/rootcontent.xsl \ examples/style/annotatedpres.xsl examples/style/theory_content.xsl \ diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index 76f6e5a78..d364ffe4b 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -385,7 +385,7 @@ let mktree selection_changed rendering_window = ignore(treeitem2#connect#select (selection_changed rendering_window uri)) ; aux treeitem2 ti - ) !content + ) (List.sort compare !content) | _ -> () in aux -- 2.39.2