editors: make the editor restarts nicer looking

mrjbq7 · Nov 15, 2024 · c1ecd9d · c1ecd9d
1 parent d013449
commit c1ecd9d
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/basis/editors/editors.factor b/basis/editors/editors.factor
@@ -14,7 +14,8 @@ SYMBOL: editor-class
 : available-editors ( -- seq )
     "editors" disk-child-vocab-names
     { "editors.ui" "editors.private" } diff
-    [ vocab-platforms supported-platform? ] filter ;
+    [ vocab-platforms supported-platform? ] filter
+    [ "editors." ?head drop ] map ;
 
 : editor-restarts ( -- alist )
     available-editors

diff --git a/extra/readline-listener/readline-listener.factor b/extra/readline-listener/readline-listener.factor
@@ -52,7 +52,7 @@ M: readline-reader prompt.
     named-colors prefixed ;
 
 : prefixed-editors ( prefix -- editors )
-    available-editors [ "editors." ?head drop ] map prefixed ;
+    available-editors prefixed ;
 
 : prefixed-chars ( prefix -- chars )
     name-map keys prefixed ;