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.
required space is already part of Position.here;
authorwenzelm
Fri, 01 Apr 2016 18:46:25 +0200
changeset 62803 5f73bf6ba98b
parent 62802 ddc58826cbe9
child 62804 7b9c5416f30e
required space is already part of Position.here;
src/Pure/General/position.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/General/position.ML	Fri Apr 01 18:43:54 2016 +0200
+++ b/src/Pure/General/position.ML	Fri Apr 01 18:46:25 2016 +0200
@@ -214,7 +214,7 @@
     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
   end;
 
-val here_list = space_implode " " o map here;
+val here_list = implode o map here;
 
 
 (* range *)
isabelle