src/Pure/ProofGeneral/pgip_isabelle.ML

 signature PGIP_ISABELLE =
 sig
     val isabelle_pgml_version_supported : string
     val isabelle_pgip_version_supported : string
     val systemid : string
-    val accepted_inputs : (string * bool * (string list)) list 
+    val accepted_inputs : (string * bool * (string list)) list
 
     val location_of_position : Position.T -> PgipTypes.location
 
     (* Additional types of objects in Isar scripts *)
 

     val ObjFormalComment : PgipTypes.objtype
     val ObjClass : PgipTypes.objtype
     val ObjTheoremSet : PgipTypes.objtype
     val ObjOracle : PgipTypes.objtype
     val ObjLocale : PgipTypes.objtype
-	
+
 end
 
 structure PgipIsabelle : PGIP_ISABELLE =
 struct
 
 val isabelle_pgml_version_supported = "2.0";
 val isabelle_pgip_version_supported = "2.0"
 val systemid = "Isabelle"
 
+
 (** Accepted commands **)
 
 local
 
     (* These element names are a subset of those in pgip_input.ML.
        They must be handled in proof_general_pgip.ML/process_pgip_element. *)
-						    
+
     val accepted_names =
     (* not implemented: "askconfig", "forget", "restoregoal" *)
     ["askpgip","askpgml","askprefs","getpref","setpref",
      "proverinit","proverexit","startquiet","stopquiet",
      "pgmlsymbolson", "pgmlsymbolsoff",
-     "dostep", "undostep", "redostep", "abortgoal", 
+     "dostep", "undostep", "redostep", "abortgoal",
      "askids", "showid", "askguise",
      "parsescript",
      "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
      "doitem", "undoitem", "redoitem", "abortheory",
      "retracttheory", "loadfile", "openfile", "closefile",
      "abortfile", "retractfile", "changecwd", "systemcmd"];
 
-    fun element_async p = 
-	false (* single threaded only *)
+    fun element_async p =
+        false (* single threaded only *)
 
     fun supported_optional_attrs p = (case p of
-					  "undostep" => ["times"]
-					(* TODO: we could probably extend these too:
-					| "redostep" => ["times"]
-					| "undoitem" => ["times"]
-					| "redoitem" => ["times"] *)
-				        | _ => [])
+                                          "undostep" => ["times"]
+                                        (* TODO: we could probably extend these too:
+                                        | "redostep" => ["times"]
+                                        | "undoitem" => ["times"]
+                                        | "redoitem" => ["times"] *)
+                                        | _ => [])
 in
-val accepted_inputs = 
+val accepted_inputs =
     (map (fn p=> (p, element_async p, supported_optional_attrs p))
          accepted_names);
 end
 
 
-fun location_of_position pos = 
+fun location_of_position pos =
     let val line = Position.line_of pos
-	val (url,descr) = 
-	    (case Position.file_of pos of
-	       NONE => (NONE, NONE)
-	     | SOME fname => 
-	       let val path = Path.explode fname in
-		 case ThyLoad.check_file NONE path of
-		   SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
-		 | NONE => (NONE, SOME fname)
-	       end);
+        val (url,descr) =
+            (case Position.file_of pos of
+               NONE => (NONE, NONE)
+             | SOME fname =>
+               let val path = Path.explode fname in
+                 case ThyLoad.check_file NONE path of
+                   SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
+                 | NONE => (NONE, SOME fname)
+               end);
     in
-	{ descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
+        { descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
     end
 
 
 val [ObjTheoryBody,
      ObjTheoryDecl,

      ObjFormalComment,
      ObjClass,
      ObjTheoremSet,
      ObjOracle,
      ObjLocale] =
-    map PgipTypes.ObjOther 
-	["theory body", 
-	 "theory declaration",
-	 "theory subsection",
-	 "proof body",
-	 "formal comment",
-	 "class",
-	 "theorem set declaration",
-	 "oracle",
-	 "locale"];
+    map PgipTypes.ObjOther
+        ["theory body",
+         "theory declaration",
+         "theory subsection",
+         "proof body",
+         "formal comment",
+         "class",
+         "theorem set declaration",
+         "oracle",
+         "locale"];
 
-	
 end
-