src/Pure/Thy/latex.ML
changeset 67355 4c8280aaf6ad
parent 67353 95f5f4bec7af
child 67358 dfee70a24f0c
equal deleted inserted replaced
67354:f243af7b5be3 67355:4c8280aaf6ad
    74         |> fold output texts |> #1 |> rev |> cat_lines)
    74         |> fold output texts |> #1 |> rev |> cat_lines)
    75   end;
    75   end;
    76 
    76 
    77 end;
    77 end;
    78 
    78 
    79 fun enclose_body bg en body = string bg :: body @ [string en];
    79 fun enclose_body bg en body =
       
    80   (if bg = "" then [] else [string bg]) @ body @
       
    81   (if en = "" then [] else [string en]);
    80 
    82 
    81 
    83 
    82 (* output name for LaTeX macros *)
    84 (* output name for LaTeX macros *)
    83 
    85 
    84 val output_name =
    86 val output_name =