...

[helm.git] / helm / papers / calculemus-2003 / hbugs-calculemus-2003.tex

diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
index 9ebbc9403806da2087dd6eaf7af737e92727c553..b6425289fab3b9fce7c0a0da5115e44ef13985c7 100644 (file)
--- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
+++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
@@ -430,12 +430,13 @@ the \hbugs{} architecture.
     pass the control to a second thread, created on the fly, to handle the
     incoming request following the classical one-thread-per-request approach in
     web servers design.
-    If the received request is a Start\_musing one a new thread is spawned to
-    handle it and the thread in duty to handle the HTTP request returns an HTTP
-    response containing an identifier of the just started musing.
-    Otherwise, if the received request is a Stop\_musing one, it should carry a
-    musing identifier used to identify the thread responsible for a musing. Once
-    identified that thread gets killed and an HTTP response could be returned.
+    If the received request is \texttt{Start\_musing}, a new thread is
+    spawned to handle it and the thread in duty to handle the HTTP request
+    returns an HTTP response containing an identifier of the just started
+    musing. Otherwise, if the received request is \texttt{Stop\_musing},
+    it carries a \texttt{musing} identifier used to identify the thread
+    responsible for a \texttt{musing}; that thread gets killed and an HTTP
+    response is returned.
 
     This architecture turns out to be scalable and allows the running threads
     to share the cache of loaded (and type-checked) theorems.