src/Doc/System/Server.thy

   connections and may be shared by different clients, as long as the internal
   session identifier is known.
 
   \<^item> \<^bold>\<open>type\<close> \<open>node = {node_name: string, theory_name: string}\<close> represents the
   internal node name of a theory. The \<open>node_name\<close> is derived from the
-  canonical theory file-name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close> after
+  canonical theory file-name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/Examples/Seq.thy"\<close> after
   normalization within the file-system). The \<open>theory_name\<close> is the
-  session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>).
+  session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-Examples.Seq\<close>).
 
   \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
   int, warned: int, failed: int, finished: int, canceled: bool, consolidated:
   bool, percentage: int}\<close> represents a formal theory node status of the PIDE
   document model as follows.

 
   \<^medskip>
   The \<open>master_dir\<close> field specifies the master directory of imported theories:
   it acts like the ``current working directory'' for locating theory files.
   This is irrelevant for \<open>theories\<close> with an absolute path name (e.g.\
-  \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close>) or session-qualified theory name (e.g.\
-  \<^verbatim>\<open>"HOL-ex/Seq"\<close>).
+  \<^verbatim>\<open>"~~/src/HOL/Examples/Seq.thy"\<close>) or session-qualified theory name (e.g.\
+  \<^verbatim>\<open>"HOL-Examples.Seq"\<close>).
 
   \<^medskip>
   The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
   default is suitable for classic console output. Formatting happens at the
   end of \<^verbatim>\<open>use_theories\<close>, when all prover messages are exported to the client.

 
 text \<open>
   Process some example theory from the Isabelle distribution, within the
   context of an already started session for Isabelle/HOL (see also
   \secref{sec:command-session-start}):
-  @{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/ex/Seq"]}\<close>}
+  @{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/Examples/Seq"]}\<close>}
 
   \<^medskip>
   Process some example theories in the context of their (single) parent
   session: