# HG changeset patch
# User aspinall
# Date 1164193319 -3600
# Node ID abaf43b011ee7f98f60e2900a85f4ff21b18a484
# Parent  42dd50268c8b9f659e66cfeff1f0ba85c2ff5c7b
Fix to local file URI syntax.  Add first part of lexicalstructure command support.

diff -r 42dd50268c8b -r abaf43b011ee src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Nov 22 10:22:04 2006 +0100
+++ b/src/Pure/proof_general.ML	Wed Nov 22 12:01:59 2006 +0100
@@ -264,7 +264,7 @@
 
   val thyname_attr = pair "thyname";
   val url_attr = pair "url";
-  fun localfile_url_attr path = url_attr ("file:///" ^ path);
+  fun localfile_url_attr abspath = url_attr ("file://" ^ abspath);
 in
 
 fun setup_messages () =
@@ -623,6 +623,24 @@
    ];
 end;
 
+(** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
+
+fun lexicalstructure_keywords () = 
+    let val commands = OuterSyntax.dest_keywords ()
+	fun category_of k = if (k mem commands) then "major" else "minor"
+         (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
+    	fun keyword_elt (keyword,help,kind,_) = 
+  	    XML.element "keyword" [("word", keyword), ("category", category_of kind)]
+	  	    [XML.element "shorthelp" [] [XML.text help]]
+        in 	    	    
+            (* Also, note we don't call init_outer_syntax here to add interface commands,
+            but they should never appear in scripts anyway so it shouldn't matter *)
+            XML.element "lexicalstructure" [] (map keyword_elt (OuterSyntax.dest_parsers()))
+        end
+
+(* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
+   hooks needed in outer_syntax.ML to do that. *)
+
 
 (* Configuration: GUI config, proverinfo messages *)
 
@@ -648,7 +666,9 @@
             []
     in
         if exists then
-            (issue_pgips [proverinfo]; issue_pgips [File.read path])
+            (issue_pgips [proverinfo]; 
+	     issue_pgips [File.read path];
+	     issue_pgips [lexicalstructure_keywords()])
         else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
     end;
 end
@@ -738,6 +758,7 @@
 end
 
 
+
 (** Parsing proof scripts without execution **)
 
 (* Notes.
@@ -1127,6 +1148,7 @@
 
 
 
+
 (**** PGIP:  Interface -> Isabelle/Isar ****)
 
 exception PGIP of string;
@@ -1489,4 +1511,5 @@
 
 end;
 
+
 end;