From b8524484c5c68803383add14d526ead17c11df4a Mon Sep 17 00:00:00 2001
From: Lutz Kettner <kettner@mpi-sb.mpg.de>
Date: Thu, 19 Jun 1997 16:14:59 +0000
Subject: [PATCH] \stl macro added.

---
 Packages/Manual_tools/format/cc_manual.sty | 1 +
 Packages/Manual_tools/src/extract_lex.yy   | 5 +++++
 Packages/Manual_tools/src/html_lex.yy      | 7 +++++++
 3 files changed, 13 insertions(+)

diff --git a/Packages/Manual_tools/format/cc_manual.sty b/Packages/Manual_tools/format/cc_manual.sty
index b9f50c49edf..592e5032748 100644
--- a/Packages/Manual_tools/format/cc_manual.sty
+++ b/Packages/Manual_tools/format/cc_manual.sty
@@ -574,6 +574,7 @@
 %\def\Q{\mbox{$\Bbb{Q}$}}  %% zusammen mit usepackage{amssymb}
 %\def\E{\mbox{$\Bbb{E}$}}  %% zusammen mit usepackage{amssymb}
 
+\newcommand{\stl}{{\sc STL}}
 \newcommand{\leda}{{\sc Leda}}
 \newcommand{\cgal}{{\sc Cgal}}
 \newcommand{\protocgal}{{\sc C++gal}}
diff --git a/Packages/Manual_tools/src/extract_lex.yy b/Packages/Manual_tools/src/extract_lex.yy
index df596cccdcc..c21435e1e99 100644
--- a/Packages/Manual_tools/src/extract_lex.yy
+++ b/Packages/Manual_tools/src/extract_lex.yy
@@ -354,6 +354,11 @@ blockintro      [\{][\\]((tt)|(em)|(it)|(sc)|(sl))
 		    yylval.string.len  = 2;
 		    return STRING;
                  }
+[\\]stl{w}         {
+	            yylval.string.text = "STL";
+		    yylval.string.len  = 3;
+		    return STRING;
+                 }
 [\\]leda{w}         {
 	            yylval.string.text = "LEDA";
 		    yylval.string.len  = 4;
diff --git a/Packages/Manual_tools/src/html_lex.yy b/Packages/Manual_tools/src/html_lex.yy
index 4623aff41a6..c993d99bbee 100644
--- a/Packages/Manual_tools/src/html_lex.yy
+++ b/Packages/Manual_tools/src/html_lex.yy
@@ -827,6 +827,13 @@ calblockintro   ([\{][\\](cal))|([\\]mathcal[\{])
 		    yylval.string.len  = -1;
 		    return STRING;
                  }
+[\\]stl/{noletter}        {
+		    skipspaces();
+	            /* yylval.string.text = "<TT>STL</TT>"; */
+	            yylval.string.text = "STL";
+		    yylval.string.len  = -1;
+		    return STRING;
+                 }
 [\\]leda/{noletter}        {
 		    skipspaces();
 	            /* yylval.string.text = "<TT>LEDA</TT>"; */