# HG changeset patch
# User wenzelm
# Date 1621971841 -7200
# Node ID 546e1e5916351a045e58936965b89bd0a869680b
# Parent  a383c4340c250d072769a408a9ed7fd9cb195362
more direct index_entry: no positions required -- text is eventually moved to .ind file;

diff -r a383c4340c25 -r 546e1e591635 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue May 25 21:32:21 2021 +0200
+++ b/src/Pure/Thy/latex.ML	Tue May 25 21:44:01 2021 +0200
@@ -31,7 +31,6 @@
   val theory_entry: string -> string
   val index_escape: string -> string
   type index_item = {text: text, like: string}
-  val index_item: index_item -> text
   type index_entry = {items: index_item list, def: bool}
   val index_entry: index_entry -> text
   val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
@@ -265,15 +264,16 @@
 fun index_item (item: index_item) =
   let
     val like_text =
-      if #like item = "" then []
-      else [string (index_escape (#like item) ^ "@")];
-  in block (like_text @ [map_text index_escape (#text item)]) end;
+      if #like item = "" then ""
+      else index_escape (#like item) ^ "@";
+    val item_text = index_escape (output_text [#text item]);
+  in like_text ^ item_text end;
 
 fun index_entry (entry: index_entry) =
-  (separate (string "!") (map index_item (#items entry)) @
-    [string ("|" ^ index_escape (if #def entry then "isaindexdef" else "isaindexref"))])
-  |> enclose_block "\\index{" "}";
-
+  (space_implode "!" (map index_item (#items entry)) ^
+    "|" ^ index_escape (if #def entry then "isaindexdef" else "isaindexref"))
+  |> enclose "\\index{" "}"
+  |> string;
 
 fun index_binding NONE = I
   | index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref"));