# HG changeset patch
# User wenzelm
# Date 1347397165 -7200
# Node ID 2750756db9c56b13972a27bffc73769f58f9bd00
# Parent  a600c017f814980be05eae143042eee8bab3be53
more precise sections;

diff -r a600c017f814 -r 2750756db9c5 etc/options
--- a/etc/options	Tue Sep 11 22:54:12 2012 +0200
+++ b/etc/options	Tue Sep 11 22:59:25 2012 +0200
@@ -1,6 +1,6 @@
 (* :mode=isabelle-options: *)
 
-section {* Document preparation *}
+section "Document Preparation"
 
 option browser_info : bool = false
   -- "generate theory browser information"
@@ -47,7 +47,7 @@
   -- "additional print modes for prover output (separated by commas)"
 
 
-section {* Parallel checking *}
+section "Parallel Checking"
 
 option threads : int = 0
   -- "maximum number of worker threads for prover process (0 = hardware max.)"
@@ -59,7 +59,7 @@
   -- "threshold for sub-proof parallelization"
 
 
-section {* Detail of proof recording *}
+section "Detail of Proof Recording"
 
 option proofs : int = 1
   -- "level of detail for proof objects: 0, 1, 2"
@@ -69,7 +69,7 @@
   -- "skip over proofs"
 
 
-section {* Global session parameters *}
+section "Global Session Parameters"
 
 option condition : string = ""
   -- "required environment variables for subsequent theories (separated by commas)"
@@ -81,7 +81,7 @@
   -- "timeout for session build job (seconds > 0)"
 
 
-section {* Editor reactivity *}
+section "Editor Reactivity"
 
 option editor_load_delay : real = 0.5
   -- "delay for file load operations (new buffers etc.)"
diff -r a600c017f814 -r 2750756db9c5 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Sep 11 22:54:12 2012 +0200
+++ b/src/Pure/System/options.scala	Tue Sep 11 22:59:25 2012 +0200
@@ -85,7 +85,7 @@
     val option_entry: Parser[Options => Options] =
     {
       command(SECTION) ~! text ^^
-        { case _ ~ a => (options: Options) => options.set_section(a.trim) } |
+        { case _ ~ a => (options: Options) => options.set_section(a) } |
       command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
       keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
         { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) }
diff -r a600c017f814 -r 2750756db9c5 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue Sep 11 22:54:12 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Sep 11 22:59:25 2012 +0200
@@ -19,7 +19,7 @@
   -- "global delay for Swing tooltips"
 
 
-section {* Editor document view *}
+section "Editor Document View"
 
 option color_outdated : string = "EEE3E3FF"
 option color_unprocessed : string = "FFA0A0FF"